/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | FinalTag-sig.sml | 3 type tag type 5 val axioms_of : tag -> string Nonce.t list 6 val dep_of : tag -> Dep.dep 7 val dest_tag : tag -> string list * string list 8 val isEmpty : tag -> bool 9 val isDisk : tag -> bool 10 val ax_tag : string Nonce.t -> tag 11 val set_dep : Dep.dep -> tag -> tag 12 val read : string -> tag [all...] |
H A D | Tag.sig | 3 type tag type 5 val axioms_of : tag -> string Nonce.t list 6 val dep_of : tag -> Dep.dep 7 val dest_tag : tag -> string list * string list 8 val empty_tag : tag 9 val isEmpty : tag -> bool 10 val isDisk : tag -> bool 11 val ax_tag : string Nonce.t -> tag 12 val set_dep : Dep.dep -> tag -> tag [all...] |
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | FlagDB.sig | 5 type 'a tag 7 val peek : t -> 'a tag -> string -> ('a * string) option 8 val update : string -> ('a tag * 'a) -> t -> t 9 val update_new : {desc: string, name : string} -> 'a tag * 'a -> t -> t 12 val string : string tag 13 val int : int tag 14 val bool : bool tag 15 val stringopt : string option tag 16 val mkTag : string -> 'a tag
|
H A D | FlagDB.sml | 7 type 'a tag = 15 fun update nm (tag, v:'a) t = 17 val u = tagInject tag v 22 fun update_new {desc,name} (tag, v) t = 24 val u = tagInject tag v 26 Symtab.update (name, (u, desc ^ " (" ^ tagDesc tag ^ ")")) t 29 fun peek t tag nm = 32 | SOME (u,d) => Option.map (fn v => (v, d)) (tagProject tag u) 42 val string : string tag = mkTag "string" 43 val int : int tag [all...] |
/seL4-l4v-master/seL4/libsel4/include/sel4/ |
H A D | faults.h | 13 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getFault(seL4_MessageInfo_t tag) argument 16 switch (seL4_MessageInfo_get_label(tag)) { 33 return seL4_getArchFault(tag); 38 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isDebugException_tag(seL4_MessageInfo_t tag) argument 40 return seL4_MessageInfo_get_label(tag) == seL4_Fault_DebugException; 44 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVMFault_tag(seL4_MessageInfo_t tag) argument 46 return seL4_MessageInfo_get_label(tag) == seL4_Fault_VMFault; 49 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isUnknownSyscall_tag(seL4_MessageInfo_t tag) argument 51 return seL4_MessageInfo_get_label(tag) == seL4_Fault_UnknownSyscall; 54 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isUserException_tag(seL4_MessageInfo_t tag) argument 59 seL4_isNullFault_tag(seL4_MessageInfo_t tag) argument 64 seL4_isCapFault_tag(seL4_MessageInfo_t tag) argument 70 seL4_isTimeoutFault_tag(seL4_MessageInfo_t tag) argument [all...] |
H A D | deprecated.h | 54 return seL4_GetIPCBuffer()->tag; 58 seL4_SetTag(seL4_MessageInfo_t tag) argument 60 seL4_GetIPCBuffer()->tag = tag; 78 return seL4_isVMFault_tag(seL4_GetIPCBuffer()->tag); 82 seL4_isPageFault_Tag(seL4_MessageInfo_t tag) argument 84 return seL4_isVMFault_tag(tag); 88 seL4_isExceptIPC_Tag(seL4_MessageInfo_t tag) argument 90 return seL4_isUnknownSyscall_tag(tag); 106 seL4_IsArchSyscallFrom(seL4_MessageInfo_t tag) argument 112 seL4_IsArchExceptionFrom(seL4_MessageInfo_t tag) argument [all...] |
H A D | shared_types.h | 12 seL4_MessageInfo_t tag; member in struct:seL4_IPCBuffer_
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUG.sig | 21 val assemblyCodeTag : bool Universal.tag 22 val bindingCounterTag : (unit -> FixedInt.int) Universal.tag 23 val codetreeAfterOptTag : bool Universal.tag 24 val codetreeTag : bool Universal.tag 25 val createPrintFunctionsTag : bool Universal.tag 26 val debugTag : bool Universal.tag 28 val errorDepthTag : FixedInt.int Universal.tag 29 val fileNameTag : string Universal.tag 30 val getParameter : 'a Universal.tag -> Universal.universal list -> 'a 31 val icodeTag : bool Universal.tag [all...] |
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
H A D | faults.h | 13 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag) argument 15 switch (seL4_MessageInfo_get_label(tag)) { 62 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVGICMaintenance_tag(seL4_MessageInfo_t tag) argument 64 return seL4_MessageInfo_get_label(tag) == seL4_Fault_VGICMaintenance; 67 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVCPUFault_tag(seL4_MessageInfo_t tag) argument 69 return seL4_MessageInfo_get_label(tag) == seL4_Fault_VCPUFault;
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
H A D | faults.h | 13 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag) argument 15 switch (seL4_MessageInfo_get_label(tag)) { 62 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVGICMaintenance_tag(seL4_MessageInfo_t tag) argument 64 return seL4_MessageInfo_get_label(tag) == seL4_Fault_VGICMaintenance; 67 LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVCPUFault_tag(seL4_MessageInfo_t tag) argument 69 return seL4_MessageInfo_get_label(tag) == seL4_Fault_VCPUFault;
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Thread_Data.sml | 20 abstype 'a var = Var of 'a option Universal.tag 23 fun var () : 'a var = Var (Universal.tag ()); 25 fun get (Var tag) = 26 (case Thread.Thread.getLocal tag of 30 fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
|
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | MB_Monitor.sig | 6 genLogFile : {tag:string,dir:string} -> string,
|
H A D | ProcessMultiplexor.sml | 16 type 'a job = {tag : string, command : command, update : 'a * bool -> 'a, 23 tag : string, 52 fun from tag command update starttime lastevent out err 54 {tag = tag, command = command, update = update, starttime = starttime, 58 tag = 59 {tag = tag, command = command, update = update, starttime = starttime, 62 fun to f {tag, command, update, starttime, lastevent, out, 64 f tag comman 158 val {tag, command, update, dir} = j value [all...] |
H A D | MB_Monitor.sml | 92 fun polish0 tag = 93 trashsfxes ["Theory", "Theory.sig", "Theory.sml", "Theory.dat"] tag 177 fn (jk as (_, tag),{status,...}) => 178 print (polish tgtw tag ^ statusString status ^ " ") 185 | (jk as (_, tag),{tb,status,...}) :: _ => 190 print (polish tgtw tag ^ 211 fun taginfo tag colour pfx s = 213 squash_to (Width() - (7 + String.size pfx) - 1) (delsml_sfx tag) ^ 217 StartJob (jk as (_, tag), {dir}) => 219 val strm = TextIO.openOut (genLogFile{tag [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | GrammarAncestry.sml | 8 val tag = "GrammarAncestry" value 16 thydataty = tag, merge = op @, 24 case Theory.LoadableThyData.segment_data{thy=thy, thydataty=tag} of 31 Theory.LoadableThyData.set_theory_data{thydataty = tag, data = write sl}
|
H A D | AncestryData.sml | 8 tag : string, initial_values : (string * 'value) list, 36 apply_delta : 'd -> 'v -> 'v, tag : string, 46 val _ = DPRINT ("Calling " ^ #tag info ^ ":merge[" ^ 84 val {tag,apply_delta_hook,delta_side_effects,apply_delta,get_deltas, value 96 val _ = DPRINT (tag ^ ":onload(" ^ thyname ^ 106 ("make("^tag^") got bad ancestor sexp") 109 val _ = DPRINT (tag ^ ":onload(" ^ thyname ^ 135 val {tag, apply_delta, initial_values, ...} = info value 145 {tag = tag, apply_delta_hoo [all...] |
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 33 tag: String = "", 92 val tag_option = if (tag == "") "" else " -t " + Bash.string(tag) 112 var tag = "" 127 -t TAG docker build tag 144 "t:" -> (arg => tag = arg), 156 more_packages = more_packages, tag = tag, verbose = verbose)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 33 tag: String = "", 92 val tag_option = if (tag == "") "" else " -t " + Bash.string(tag) 112 var tag = "" 127 -t TAG docker build tag 144 "t:" -> (arg => tag = arg), 156 more_packages = more_packages, tag = tag, verbose = verbose)
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | faults.h | 13 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag) argument 15 switch (seL4_MessageInfo_get_label(tag)) {
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/ |
H A D | faults.h | 14 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag) argument 16 switch (seL4_MessageInfo_get_label(tag)) {
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/ |
H A D | faults.h | 14 LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag) argument 16 switch (seL4_MessageInfo_get_label(tag)) {
|
/seL4-l4v-master/graph-refine/ |
H A D | c_rodata.py | 18 tag = p.node_tags[n][0] 19 is_C = tag == 'C' or p.hook_tag_hints.get (tag, None) == 'C'
|
H A D | problem.py | 50 def alloc_node (self, tag, detail, loop_id = None, hint = None): 54 self.node_tags[name] = (tag, detail) 55 self.node_tag_revs.setdefault ((tag, detail), []) 56 self.node_tag_revs[(tag, detail)].append (name) 67 def clone_function (self, fun, tag): 73 self.node_tags[n] = (tag, detail) 74 self.node_tag_revs.setdefault ((tag, detail), []) 75 self.node_tag_revs[(tag, detail)].append (n) 76 self.outputs[tag] = fun.outputs 77 self.entries = [(fun.entry, tag, fu [all...] |
H A D | rep_graph.py | 239 pc1 = rep.get_pc (visit1, tag = tag1) 243 pc2 = rep.get_pc (visit2, tag = tag2) 251 x_pc_env = rep.get_node_pc_env (xvis[0], tag = xvis[1]) 252 y_pc_env = rep.get_node_pc_env (yvis[0], tag = yvis[1]) 261 x_pc = rep.get_pc (xvis[0], tag = xvis[1]) 262 y_pc = rep.get_pc (yvis[0], tag = yvis[1]) 269 def check_vis_is_vis (((n, vc), tag)): 339 def get_tag_vcount (self, (n, vcount), tag): 340 if tag == None: 341 tag [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ASN1.sml | 38 (* Parse the tag and length information to extract the first tag/value pair from the 42 (* Parse the tag and length information to extract the first tag/value pair from the 45 {tag: tagType, data: Word8VectorSlice.slice, remainder: Word8VectorSlice.slice} option 52 (* Encode a tag/value pair. *) 113 (* The tag is the bottom five bits except that if it is 0x1f 114 the tag is encoded in subsequent bytes. *) 117 0w31 => (* This is a long-format tag *) 125 val tag' [all...] |