Searched refs:tag (Results 26 - 50 of 142) sorted by relevance

123456

/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/
H A Dboot_sys.c674 multiboot2_tag_t const * tag = (multiboot2_tag_t *)(mbi2 + 1); local
687 while (tag < tag_e && tag->type != MULTIBOOT2_TAG_END) {
688 word_t const behind_tag = (word_t)tag + sizeof(*tag);
690 if (tag->type == MULTIBOOT2_TAG_CMDLINE) {
693 } else if (tag->type == MULTIBOOT2_TAG_ACPI_1) {
694 if (ACPI_V1_SIZE == tag->size - sizeof(*tag)) {
695 memcpy(&boot_state.acpi_rsdp, (void *)behind_tag, tag
[all...]
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParserGenpreds.sml38 fun mk_holfoot_ap_list_seg_absyn (tag, exp1, exp2) =
40 tag, exp1, Absyn.mk_AQ holfoot_data_list___EMPTY_tm, exp2]);
55 (* lseg(tag;x,y) *)
57 fn [tag,exp1,exp2] => mk_holfoot_ap_list_seg_absyn (
58 tag,
63 fun mk_holfoot_ap_data_list_seg_absyn (tag, exp1, dtag, data, exp2) =
65 tag, exp1, mk_list [Absyn.mk_pair (dtag, data)], exp2]);
87 (* data_lseg(tag;x,dtag:data,y) *)
93 fn [tag,exp1,dtag,data,exp2] => mk_holfoot_ap_data_list_seg_absyn (
94 tag,
[all...]
/seL4-l4v-10.1.1/graph-refine/
H A Dstack_logic.py169 tag = p.node_tags[n][0]
170 hyp = rep_graph.pc_false_hyp ((default_n_vc (p, n), tag))
205 for tag in set ([p.node_tags[n][0] for (n, _) in n_ptrs]):
206 hyps = hyps + init_correctness_hyps (p, tag)
228 def init_correctness_hyps (p, tag):
229 (_, fname, _) = p.get_entry_details (tag)
236 if tag in pair.funs:
237 true_tag = tag
238 elif p.hook_tag_hints.get (tag, tag) i
[all...]
H A Dcheck.py31 for (tag, fname) in pairing.funs.items ():
32 p.add_entry_function (functions[fname], tag)
79 [compare_tag] = [tag for tag in p.pairing.tags if tag != 'C']
130 def consider_inline (matched_funs, tag, force_inline, skip_underspec = False):
131 return lambda (p, n): consider_inline1 (p, n, matched_funs, tag,
137 tag_map = dict ([(tag, tag) for tag i
[all...]
H A Ddebug.py33 for (entry, tag, _, inputs) in p.entries:
39 print 'Vars deps escaped in %s in %s: %s' % (tag,
91 tags = set ([tag for (tag, n, vc) in rep.node_pc_env_order])
94 for tag in tags:
95 print "Walking %s in model" % tag
96 n_vcs = walk_model (rep, tag, m)
115 def walk_model (rep, tag, m):
117 if tag2 == tag
119 rep.get_pc ((n, vc), tag))
[all...]
H A Dtrace_refute.py140 tag = '%s_%d_%s' % (fname, i, pair_tag)
141 tag = syntax.fresh_name (tag, all_tags)
142 next_tags[pair_tag] = tag
143 p.add_entry_function (functions[fname], tag)
144 p.hook_tag_hints[tag] = pair_tag
145 p.replay_inline_script (tag, scripts[pair_tag])
184 def get_vis (p, n, tag = None, focused_loops = None):
186 if not tag:
187 tag
[all...]
H A Dloop_bounds.py147 tag = p.node_tags[p_n][0]
164 epc = rep.get_pc (('Err', restrs3), tag = tag)
191 (tag, _) = p.node_tags[split]
196 checks = (check.single_loop_induct_step_checks (p, restrs, hyps, tag,
198 + check.single_loop_induct_base_checks (p, restrs, hyps, tag,
229 (tag, _) = p.node_tags[split]
230 hyps = [h for (h, _) in linear_eq_hyps_at_visit (tag, split, eqs,
310 for (n_vc, tag) in hyp.visits ():
311 if not p.hook_tag_hints.get (tag, Non
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Dinvoke_scala.scala82 private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
86 session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
103 val (tag, result) = Invoke_Scala.method(name, msg.text)
104 fulfill(id, tag, result)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Dinvoke_scala.scala82 private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
86 session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
103 val (tag, result) = Invoke_Scala.method(name, msg.text)
104 fulfill(id, tag, result)
/seL4-l4v-10.1.1/seL4/src/kernel/
H A Dthread.c152 seL4_MessageInfo_t tag; local
156 tag = messageInfoFromWord(getRegister(sender, msgInfoRegister));
159 status = lookupExtraCaps(sender, sendBuffer, tag);
170 seL4_MessageInfo_get_length(tag));
172 tag = transferCaps(tag, caps, endpoint, receiver, receiveBuffer);
174 tag = seL4_MessageInfo_set_length(tag, msgTransferred);
175 setRegister(receiver, msgInfoRegister, wordFromMessageInfo(tag));
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DTag.sml18 (* A tag is represented by a pair (D,O,A) where O is a list of oracles *)
25 datatype tag = TAG of dep * string list * string Nonce.t list type
41 Create a tag. A tag is a string with only printable characters (as
87 number inside the tag. Other informations are retrieved from the dependency
119 Prettyprint a tag (for interactive work).
H A DFinalThm-sig.sml4 type tag type
14 val tag : thm -> tag value
110 val add_tag : tag * thm -> thm
/seL4-l4v-10.1.1/HOL4/src/0/
H A DKernelTypes.sml47 The representation of theorems. A "tag" is a pair of the oracles
52 datatype thm = THM of Tag.tag * term HOLset.set * term
/seL4-l4v-10.1.1/HOL4/src/1/
H A DRewrite.sml46 fun decompose tag th =
51 if is_eq t then [(th,tag)] else
52 if is_conj t then (op@ o (decompose tag##decompose tag) o CONJ_PAIR) th else
53 if is_neg t then [(EQF_INTRO th,tag)]
54 else [(EQT_INTRO th,tag)]
93 (map (fn (th,tag) =>
95 (appconv (Conv.REWR_CONV th,tag)))) rewrites)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DPrimitiveBddRules.sig30 val getTag : term_bdd -> Thm.tag
38 val dest_term_bdd : term_bdd -> Thm.tag * assums * varmap * Term.term * bdd.bdd
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/
H A DProcessMultiplexor.sig5 type 'a job = {tag : string, command : command, update : 'a * bool -> 'a}
H A Dmultibuild.sml30 genLogFile = (fn {tag} => loggingdir ++ safetag tag),
87 NewJob ({tag = target_s, command = shell_command c,
120 NewJob({tag = target_s,
/seL4-l4v-10.1.1/l4v/tools/c-parser/
H A Dmkrelease38 die " $0 tag" >&2
63 tag=$1
64 stem=c-parser-$tag
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/32/mode/kernel/
H A Dvspace.h30 pde_pte_tag_t tag; member in struct:createMappingEntries_ret
/seL4-l4v-10.1.1/l4v/misc/regression/
H A Dtestspec.py51 def parse_attributes(tag, env):
52 """Parse attributes such as "timeout" in the given XML tag,
58 value = tag.get(xml_name)
118 parser = parsers[doc.tag]
120 raise TestSpecParseException("Unknown tag '%s'" % doc.tag)
147 # Parse this tag as a set of tests.
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DSTRUCTVALSIG.sml303 val valueVar: values Universal.tag
304 val typeConstrVar: typeConstrSet Universal.tag
305 val fixVar: fixStatus Universal.tag
306 val structVar: structVals Universal.tag
307 val signatureVar: signatures Universal.tag
308 val functorVar: functors Universal.tag
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DDatabase.sml61 let val tag = BinIO.input1 is in value
62 case tag of
98 let val tag = BinIO.input1 is in value
99 case tag of
149 let val tag = BinIO.input1 is in value
150 case tag of
/seL4-l4v-10.1.1/seL4/src/api/
H A Dfaults.c122 seL4_MessageInfo_t tag = messageInfoFromWord(getRegister(sender, msgInfoRegister)); local
123 word_t label = seL4_MessageInfo_get_label(tag);
124 word_t length = seL4_MessageInfo_get_length(tag);
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Delf_correlate.py205 tag = p.node_tags[p_n]
206 _, x = tag
480 tag = p.node_tags[p_n]
481 return tag[1] == 'LoopReturn'
591 tag = p.node_tags[p_n]
592 f = tag[1][0]
593 g_n = tag[1][1]
/seL4-l4v-10.1.1/seL4/manual/tools/
H A Dparse_doxygen_xml.py101 def parse_list(self, para, ref_dict, tag):
291 def parse_list(self, para, ref_dict, tag):
294 output = '\\begin{%s}\n' % tag
297 output += '\\end{%s}\n' % tag
423 def parse_list(self, para, ref_dict, tag):
426 if tag == "enumerate":
428 elif tag == "itemize":

Completed in 230 milliseconds

123456