/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | ibm.sml | 5 loadPath := (concat home_dir "src/deep_embeddings") :: 6 (concat home_dir "src/translations") :: 7 (concat home_dir "src/model_check") :: 8 (concat home_dir "src/tools") ::
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/lib/Tools/ |
H A D | jedit | 11 "src-base/dockable.scala" 12 "src-base/isabelle_encoding.scala" 13 "src-base/jedit_lib.scala" 14 "src-base/pide_docking_framework.scala" 15 "src-base/plugin.scala" 16 "src-base/syntax_style.scala" 20 "src-base/Isabelle_Base.props" 21 "src-base/services.xml" 25 "src/active.scala" 26 "src/completion_popu [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Array2Signature.sml | 43 {src : 'a region, dst : 'a array, dst_row : int, dst_col : int} -> unit
|
H A D | Word8.sml | 113 fun scan radix getc src = 114 case wordScan radix getc src of 116 | SOME(res, src') => 119 else SOME(res, src')
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/lib/Tools/ |
H A D | jedit | 11 "src-base/dockable.scala" 12 "src-base/isabelle_encoding.scala" 13 "src-base/jedit_lib.scala" 14 "src-base/pide_docking_framework.scala" 15 "src-base/plugin.scala" 16 "src-base/syntax_style.scala" 20 "src-base/Isabelle_Base.props" 21 "src-base/services.xml" 25 "src/active.scala" 26 "src/completion_popu [all...] |
/seL4-l4v-10.1.1/seL4/include/object/ |
H A D | tcb.h | 128 exception_t invokeTCB_CopyRegisters(tcb_t *dest, tcb_t *src, 132 exception_t invokeTCB_ReadRegisters(tcb_t *src, bool_t suspendSource,
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | HSLScript.sml | 246 (transfer (s1,s0) (dst::dstL, src::srcL) = 247 transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`; 250 (!dst src.tdecode hs (TLDR dst src) = 251 twrite hs (inR dst) (tread hs (inE src))) /\ 252 (!dst src.tdecode hs (TSTR dst src) = 253 twrite hs (inE dst) (tread hs (inR src))) /\ 254 (tdecode hs (TMOV dst src) = 255 twrite hs (inR dst) (tread hs (roc_2_exp src))) /\ [all...] |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in 192 ( T.enter(use, nodeNo, S.addList(S.empty intOrder, src)), 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 610 src = if lhs then replace s1 old new else s1, jump = j1} 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 614 src = if lhs andalso s1 = old then new else s1}; 647 src = [Assem.TMEM (!memIndex)], 662 src = [Assem.TEMP newVarNo], 683 let val (Assem.MOVE {dst = d1, src [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | html.scala | 203 def image(src: String, alt: String = ""): XML.Elem = 204 XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) 207 def source(src: String): XML.Elem = source(text(src)) 215 def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) 366 " src: url('" + make_url(ttf_name) + "') format('truetype');") :::
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | html.scala | 203 def image(src: String, alt: String = ""): XML.Elem = 204 XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) 207 def source(src: String): XML.Elem = source(text(src)) 215 def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) 366 " src: url('" + make_url(ttf_name) + "') format('truetype');") :::
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in 192 ( T.enter(use, nodeNo, S.addList(S.empty intOrder, src)), 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 610 src = if lhs then replace s1 old new else s1, jump = j1} 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 614 src = if lhs andalso s1 = old then new else s1}; 647 src = [Assem.TMEM (!memIndex)], 662 src = [Assem.TEMP newVarNo], 683 let val (Assem.MOVE {dst = d1, src [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | regAllocation.sml | 180 fun isMoveInst (Assem.MOVE {dst = Assem.TEMP d1, src = Assem.TEMP s1}) = true 191 ( let val (dst,src) = (#def inst, #use inst) in 192 ( T.enter(use, nodeNo, S.addList(S.empty intOrder, src)), 608 fun substituteVars (Assem.OPER {oper = p, dst = d1, src = s1, jump = j1}) old new rhs lhs = 610 src = if lhs then replace s1 old new else s1, jump = j1} 612 | substituteVars (Assem.MOVE {dst = d1, src = s1}) old new rhs lhs = 614 src = if lhs andalso s1 = old then new else s1}; 647 src = [Assem.TMEM (!memIndex)], 662 src = [Assem.TEMP newVarNo], 683 let val (Assem.MOVE {dst = d1, src [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 2671 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2682 (Call("XMM",ATy(qTy,FTy 128),Var("src",CTy"xmm_mem")), 2714 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2725 (Call("XMM",ATy(qTy,FTy 128),Var("src",CTy"xmm_mem")), 2781 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2799 Var("src",CTy"xmm_mem")),qVar"state"), 2819 TP[Var("bop",CTy"sse_binop"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2837 Var("src",CTy"xmm_mem")),qVar"state"), 2857 TP[Var("bop",CTy"sse_logic"),Var("dst",FTy 3),Var("src",CTy"xmm_mem")], 2868 (Call("XMM",ATy(qTy,FTy 128),Var("src",CT [all...] |
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | cppext.cxx | 538 bvec bvec::operator=(const bvec &src) argument 540 if (&src != this) 543 roots = bvec_copy(src.roots);
|
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
H A D | RealStringCvt.sml | 34 val scan = fn getc => fn src => Option.map(fn (v, c) => (toNewDA v, c)) (scan getc src)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairLib.sml | 12 fun pairLib_ERR src msg = mk_HOL_ERR "pairLib" src msg
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Globals.sml | 180 val emitMLDir = ref (Path.concat(HOLDIR,"src/emit/ML/")) 181 val emitCAMLDir = ref (Path.concat(HOLDIR,"src/emit/Caml/"))
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | make_iss.sml | 34 val _ = (FileSys.chDir "help", FileSys.chDir "src-sml") 36 val _ = print "cleanable stuff in help/src-sml\n\n"
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl-transformations/ |
H A D | ltl_translationsScript.sml | 144 (* Translation examples/temporal_deep -> src/temporal *) 204 (* Translation examples/logic/ltl -> src/temporal *)
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | omega_automatonScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath;
|
H A D | semi_automatonScript.sml | 7 loadPath := (home_dir ^ "src/deep_embeddings") :: 8 (home_dir ^ "src/tools") :: !loadPath;
|
H A D | symbolic_kripke_structureScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath;
|
H A D | temporal_deep_simplificationsLib.sml | 8 loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/tools") :: !loadPath;
|
/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/ |
H A D | RPCTo.c | 1027 src 1045 src 1205 src 1226 src
|
/seL4-l4v-10.1.1/HOL4/examples/ |
H A D | fol.sml | 3 * of MESON. There are many more such examples in src/meson/test.sml. *
|