/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/ |
H A D | boot_sys.c | 674 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 D | holfootParserGenpreds.sml | 38 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 D | stack_logic.py | 169 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 D | check.py | 31 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 D | debug.py | 33 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 D | trace_refute.py | 140 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 D | loop_bounds.py | 147 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 D | invoke_scala.scala | 82 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 D | invoke_scala.scala | 82 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 D | thread.c | 152 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 D | Tag.sml | 18 (* 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 D | FinalThm-sig.sml | 4 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 D | KernelTypes.sml | 47 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 D | Rewrite.sml | 46 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 D | PrimitiveBddRules.sig | 30 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 D | ProcessMultiplexor.sig | 5 type 'a job = {tag : string, command : command, update : 'a * bool -> 'a}
|
H A D | multibuild.sml | 30 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 D | mkrelease | 38 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 D | vspace.h | 30 pde_pte_tag_t tag; member in struct:createMappingEntries_ret
|
/seL4-l4v-10.1.1/l4v/misc/regression/ |
H A D | testspec.py | 51 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 D | STRUCTVALSIG.sml | 303 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 D | Database.sml | 61 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 D | faults.c | 122 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 D | elf_correlate.py | 205 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 D | parse_doxygen_xml.py | 101 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":
|