/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryPP.sml | 118 (Tag.isEmpty (Thm.tag th) orelse Tag.isDisk (Thm.tag th)) 229 val (tg, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th) 377 fun pp_tag tag = 379 val dep = Tag.dep_of tag 380 val ocl = fst (Tag.dest_tag tag) 387 val (tag, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th) value 393 pp_tag tag >> add_newline >>
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | ipc.tex | 35 Every IPC message also has a tag (structure \texttt{seL4\_MessageInfo\_t}). The 36 tag consists of four fields: the label, message length, number of capabilities 57 \ipcparam{seL4\_MessageInfo\_t}{}{tag}{Message tag} 95 The situation is similar for the tag field. 98 may wish to copy the message tag from its CPU register to this field, although 147 to send is specified in the \texttt{extraCaps} field of the message tag. 171 tag. The capability itself is not transferred, so the receive slot may be used 174 If a receiver gets a message whose tag has an \texttt{extraCaps} of 2 and a
|
/seL4-l4v-10.1.1/HOL4/polyml/PolyPerf/ |
H A D | PolyPerf.cpp | 224 unsigned tag = *ptr++; local 226 switch (tag) 293 unsigned char tag = *ptr++; local 295 switch (tag) 318 unsigned char tag = *ptr++; local 320 switch (tag) 367 // Anything else is an unknown tag; skip
|
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | ROOT.sml | 51 fun dolookup (look, tag, kind) s = 53 SOME v => Universal.tagInject tag (s, v)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 24 nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; } 25 nodeData(int t, char *n, bdd v) { tag=t; name=n; val=v; } 27 int tag;
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 194 | BICTagTest of { test: backendIC, tag: word, maxTag: word } 266 val tupleTag: universal list list tag = tag() 269 | splitProps tag (hd::tl) = 270 if Universal.tagIs tag hd 272 else let val (p, l) = splitProps tag tl in (p, hd :: l) end 591 | BICTagTest { test, tag, maxTag } => 594 PrettyString (concat["TAGTEST(", Word.toString tag, ", ", Word.toString maxTag, ","]),
|
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 46 (* Property tag to indicate which arguments to a function are functions 48 val closureFreeArgsTag: int list Universal.tag = Universal.tag() 453 | insert(TagTest{test, tag, maxTag}) = BICTagTest{test=insert test, tag=tag, maxTag=maxTag} 488 { tag: word, test: codetree, caseType: caseType } option; 514 then SOME{tag=toShort c1, test=arg2, caseType = CaseWord} 519 then SOME{tag=toShort c2, test=arg1, caseType = CaseWord} 526 | findCase(BICTagTest { test, tag, maxTa [all...] |
H A D | BaseCodeTree.sml | 101 | TagTest of { test: codetree, tag: word, maxTag: word } 181 val inlineCodeTag: envSpecial tag = tag() 471 | TagTest { test, tag, maxTag } => 474 PrettyString (concat["TAGTEST(", Word.toString tag, ", ", Word.toString maxTag, ","]), 674 | mapt (TagTest{test, tag, maxTag}) = TagTest{test = mapCodetree f test, tag = tag, maxTag = maxTag }
|
H A D | BaseCodeTreeSig.sml | 111 | TagTest of { test: codetree, tag: word, maxTag: word } 183 val tupleTag: Universal.universal list list Universal.tag 184 val inlineCodeTag: envSpecial Universal.tag
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | PRETTYSIG.sml | 58 val printOutputTag : (pretty -> unit) Universal.tag 60 and compilerOutputTag: (pretty->unit) Universal.tag
|
H A D | DATATYPEREPSIG.sml | 35 val EnumForm: { tag: word, maxTag: word } -> representations;
|
H A D | COPIER.sml | 36 type 'a tag = 'a Universal.tag 38 val univEnter: univTable * 'a tag * string * 'a -> unit; 39 val univLookup: univTable * 'a tag * string -> 'a option; 57 open Universal; (* for tag record selectors *)
|
H A D | Pretty.sml | 259 val printOutputTag : (pretty -> unit) tag = tag() 261 and compilerOutputTag: (pretty->unit) tag = tag() 266 fun getTag (t: (pretty -> unit) tag) (tagList: universal list) : pretty -> unit =
|
H A D | ExportTree.sml | 107 val rootTreeTag: navigation Universal.tag = Universal.tag()
|
H A D | EXPORTTREESIG.sml | 59 val rootTreeTag: navigation Universal.tag
|
/seL4-l4v-10.1.1/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 78 fun line_error qp fname linenum tag line = 81 (print (fname^":"^Int.toString linenum^": " ^ tag ^ ": " ^ line); 154 fun foldthis ((_, (f, tag)), (b, tags)) = 158 (b andalso b', if not b' then inc tag tags else tags)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | search.py | 76 tag = p.node_tags[n][0] 77 trace ('Finding split limit: %d (%s)' % (n, tag)) 95 epc = rep.get_pc (('Err', restrs3), tag = tag) 113 trace ('No split limit found for %d (%s).' % (n, tag)) 146 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag)) 147 for tag in p.pairing.tags] 174 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag)) 175 for tag in p.pairing.tags] 963 for (tag, [all...] |
H A D | solver.py | 988 def next_hyp (self, (hyp, tag), hyp_dict): 991 hyp_dict[name] = tag 1000 raw_hyps = [(hyp2, tag) for (hyp, tag) in hyps 1151 unsat_core.extend ([tag for (_, tag) in hyps]) 1870 for (i, (ass, tag)) in enumerate (asserts): 1900 return set ([tag for (_, tag) in asserts]) 1904 hyps = [(smt_expr (hyp, env, self), tag) fo [all...] |
H A D | graph-refine.py | 43 for (tag, fname) in pair.funs.iteritems (): 45 printout ('Skipping %s, underspecified %s' % (pair, tag))
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | ParseDoc.sml | 328 fun section (tag, ss) = 329 case tag of 343 if null args andalso not (mem tag empty_ok) then 344 raise ParseError ("Empty "^tag^" field") 345 else FIELD (tag, args)
|
H A D | Doc2Html.sml | 114 | markout_section (FIELD (tag, ss)) 116 out (if tag = "DESCRIBE" then "DESCRIPTION" else tag);
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ExnPrinter.sml | 86 val printLimit: word ref list Universal.tag = Universal.tag()
|
H A D | FinalPolyML.sml | 683 val useFileTag: string option Universal.tag = Universal.tag() 749 type 'a tag = 'a Universal.tag; 2155 val structureTag: (string * PolyML.NameSpace.Structures.structureVal) Universal.tag = Universal.tag() 2156 val functorTag: (string * PolyML.NameSpace.Functors.functorVal) Universal.tag = Universal.tag() 2157 val signatureTag: (string * PolyML.NameSpace.Signatures.signatureVal) Universal.tag = Universal.tag() [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | Makefile.in | 184 libpolyml_la_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \ 215 LTCXXCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \ 224 CXXLINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \ 233 LTCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \ 242 LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Pmatch.sml | 199 fun build (prefix,tag,plist) = 202 in (prefix,tag, c'::plist') end 208 fun build (prefix,tag,plist) = 210 in (prefix,tag,list_mk_comb(c,args)::plist') end 218 fun v_to_pats (v::prefix,tag, pats) = (prefix, tag, v::pats) 350 let val (tag,tm) = dest_pattern rhs value 351 in ([(prefix,tag,[])], tm) 742 fun func (_,(tag,i),[pat]) = tag (pa [all...] |