/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | end-init-boss.sml | 32 val _ = use (HOLDIR^"/src/proofman/expandq"); 33 (* val _ = use (HOLDIR^"/src/datatype/Interactive"); *)
|
/seL4-l4v-10.1.1/isabelle/Admin/lib/Tools/ |
H A D | makedist | 164 src/Pure/System/distribution.ML src/Pure/System/distribution.scala 170 src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version 194 cp -a src src.orig 197 rm -rf src 198 mv src.orig src
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/lib/Tools/ |
H A D | makedist | 164 src/Pure/System/distribution.ML src/Pure/System/distribution.scala 170 src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version 194 cp -a src src.orig 197 rm -rf src 198 mv src.orig src
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | makefile | 8 CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | hfheader.sml | 3 val holfoot_base_dir = Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/";
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | treeSyntax.sml | 6 loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src") ::
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | msvcc.sh | 197 src=$1 234 ppsrc="$outdir/$(basename $src|sed 's/.S$/.asm/g')" 235 echo "$cl -nologo -EP $includes $defines $src > $ppsrc" 236 "$cl" -nologo -EP $includes $defines $src > $ppsrc || exit $?
|
/seL4-l4v-10.1.1/seL4/include/arch/arm/arch/64/mode/machine/ |
H A D | fpu.h | 57 static inline void loadFpuState(user_fpu_state_t *src) argument 86 : "r" (src)
|
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/arm/sel4/arch/ |
H A D | syscalls.h | 82 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 91 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 106 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 116 arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 140 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 149 arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 227 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 242 arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3); 259 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, argument 282 arm_sys_send_recv(seL4_SysReplyRecv, src, 483 seL4_Wait(seL4_CPtr src, seL4_Word *sender) argument 489 seL4_Poll(seL4_CPtr src, seL4_Word *sender) argument [all...] |
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | genUseScript.sml | 2 use "../src/portableML/GetOpt.sig"; 3 use "../src/portableML/GetOpt.sml"; 45 fun addIfReadable src fname rest = 46 if OS.FileSys.access(fname, [OS.FileSys.A_READ]) then (src,fname)::rest 49 fun ToplevelLoad {worklist, alreadySeen, acc} (src,s) = 56 {worklist = worklist |> addIfReadable src uo |> addIfReadable src ui, 61 fun load1 (S as {worklist, alreadySeen, acc}) (src,s) = 94 | SOME _ => die ("Can't handle " ^ s ^ " (from " ^ src ^ ")") 95 | NONE => ToplevelLoad S (src, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 108 fun one_stm ({oper = op1, dst = dst1, src = src1}) = 109 {oper = op1, dst = List.map filter_mems dst1, src = List.map filter_mems src1} 143 fun dec_p pt n = {oper = IR.msub, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]} 145 fun inc_p pt n = {oper = IR.madd, dst = [IR.REG pt], src = [IR.REG pt, IR.WCONST (Arbint.fromInt (4*n))]}; 159 [ {oper = IR.mmov, dst = [IR.REG (IR.fromAlias IR.ip)], src = [IR.REG (IR.fromAlias IR.sp)]}, 161 src = rs @ [IR.REG (IR.fromAlias IR.fp), IR.REG (IR.fromAlias IR.ip), 164 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.fp)], src = [IR.REG (IR.fromAlias IR.ip), IR.WCONST (Arbint.fromInt 4)]}, 175 {oper = IR.msub, dst = [IR.REG (IR.fromAlias IR.sp)], src = [IR.REG (IR.fromAlias IR.fp), IR.WCONST (Arbint.fromInt (4* (3 + length rs)))]}, 177 src = [IR.REG (IR.fromAlias IR.sp)]} 222 {oper = IR.mldr, dst = dataL, src [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/ |
H A D | build-jars | 177 ../Tools/VSCode/src/build_vscode.scala 178 ../Tools/VSCode/src/channel.scala 179 ../Tools/VSCode/src/document_model.scala 180 ../Tools/VSCode/src/dynamic_output.scala 181 ../Tools/VSCode/src/grammar.scala 182 ../Tools/VSCode/src/preview_panel.scala 183 ../Tools/VSCode/src/protocol.scala 184 ../Tools/VSCode/src/server.scala 185 ../Tools/VSCode/src/state_panel.scala 186 ../Tools/VSCode/src/vscode_javascrip [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ |
H A D | build-jars | 177 ../Tools/VSCode/src/build_vscode.scala 178 ../Tools/VSCode/src/channel.scala 179 ../Tools/VSCode/src/document_model.scala 180 ../Tools/VSCode/src/dynamic_output.scala 181 ../Tools/VSCode/src/grammar.scala 182 ../Tools/VSCode/src/preview_panel.scala 183 ../Tools/VSCode/src/protocol.scala 184 ../Tools/VSCode/src/server.scala 185 ../Tools/VSCode/src/state_panel.scala 186 ../Tools/VSCode/src/vscode_javascrip [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/riscv/sel4/arch/ |
H A D | syscalls.h | 73 riscv_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg) argument 75 register seL4_Word destptr asm("a0") = src; 88 riscv_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word argument 91 register seL4_Word src_and_badge asm("a0") = src; 229 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 238 riscv_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 254 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 264 riscv_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3); 288 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument 297 riscv_sys_recv(seL4_SysNBRecv, src, 334 seL4_Wait(seL4_CPtr src, seL4_Word *sender) argument 340 seL4_Poll(seL4_CPtr src, seL4_Word *sender) argument 388 seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) argument 422 seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) argument [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | SatSolvers.sml | 58 then Globals.HOLDIR^"/src/HolSat/sat_solvers/zchaff/zchaff.exe" 59 else Globals.HOLDIR^"/src/HolSat/sat_solvers/zchaff/zchaff", 62 then Globals.HOLDIR^"/src/HolSat/sat_solvers/zc2hs/zc2hs.exe" 63 else Globals.HOLDIR^"/src/HolSat/sat_solvers/zc2hs/zc2hs"), 85 then Globals.HOLDIR^"/src/HolSat/sat_solvers/minisat/minisat.exe" 86 else Globals.HOLDIR^"/src/HolSat/sat_solvers/minisat/minisat",
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 77 x86_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info) argument 89 : "+d" (src) 97 x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, seL4_Word *out_mr2) argument 117 "d" (src) 232 x86_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr1, seL4_Word *out_mr2) argument 247 "b" (src) 341 seL4_Recv(seL4_CPtr src, seL4_Word* sender) argument 348 x86_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &mr0, &mr1); 361 seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, argument 369 x86_sys_recv(seL4_SysRecv, src, 386 seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) argument [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Int.sml | 208 fun scan radix getc src = 216 fun read_digits src acc isOk = 217 case getc src of 218 NONE => if isOk then SOME(acc, src) else NONE 219 | SOME(ch, src') => 222 then read_digits src' 225 if isOk then SOME(acc, src) else NONE 227 fun read_hex_digits src acc isOk = 228 case getc src of 229 NONE => if isOk then SOME(acc, src) els [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | SALGen.sml | 71 fun mk_instr_spec (entry_l,exit_l) (dest,src) = 74 val value = mk_pair (src, dest) 75 val instr = list_mk_comb (inst [alpha |-> ty] asg_tm, [entry_l, dest, src, exit_l]) 80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest} 123 fun mk_cond_spec (entry_l,exit_l) (dest,src) args = 125 val (J,M1,M2) = dest_cond src 164 mk_spec (entry_l,exit_l) (dest,src) args = 165 if is_atomic src orelse is_pair src then 166 mk_instr_spec (entry_l,exit_l) (dest,src) [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/ |
H A D | Makefile | 13 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/num/reduce/Manual/ |
H A D | Makefile | 6 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
H A D | syscalls.h | 96 arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg) argument 98 register seL4_Word destptr asm("r0") = src; 111 arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3) argument 113 register seL4_Word src_and_badge asm("r0") = src;
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/ |
H A D | syscalls.h | 96 arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg) argument 98 register seL4_Word destptr asm("x0") = src; 111 arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3) argument 113 register seL4_Word src_and_badge asm("x0") = src;
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
H A D | syscalls.h | 96 arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg) argument 98 register seL4_Word destptr asm("r0") = src; 111 arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info, seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3) argument 113 register seL4_Word src_and_badge asm("r0") = src;
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/ |
H A D | PortableIsabelle.sml | 5 Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/ |
H A D | PortableIsabelle.sml | 5 Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
|