| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64Script.sml | 187 (Call
189 Call("INTERRUPT_EXCEPTION",CTy"exception",LW(0,8))),
196 (Call
198 Call("INTERRUPT_EXCEPTION",CTy"exception",LW(6,8))),
205 (Call
207 Call("INTERRUPT_EXCEPTION",CTy"exception",LW(13,8))),
214 (Call
216 Call("INTERRUPT_EXCEPTION",CTy"exception",LW(19,8))),
250 Call("reg'MXCSR",F32,Var("x",CTy"MXCSR")))
254 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | armScript.sml | 409 Bop(Ge,Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
430 Bop(Ge,Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
465 Call("reg'PSR",F32,Var("x",CTy"PSR")))
469 Call("rec'PSR",CTy"PSR",Var("x",F32)))
518 Call("reg'SCTLR",F32,Var("x",CTy"SCTLR")))
522 Call("rec'SCTLR",CTy"SCTLR",Var("x",F32)))
562 Call("reg'HSCTLR",F32,Var("x",CTy"HSCTLR")))
566 Call("rec'HSCTLR",CTy"HSCTLR",Var("x",F32)))
582 Call("reg'HSR",F32,Var("x",CTy"HSR")))
586 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/ |
| H A D | cheriScript.sml | 476 Call("reg'EntryLo",F64,Var("x",CTy"EntryLo")))
480 Call("rec'EntryLo",CTy"EntryLo",Var("x",F64)))
497 Call("reg'Index",F32,Var("x",CTy"Index")))
501 Call("rec'Index",CTy"Index",Var("x",F32)))
516 Call("reg'Random",F32,Var("x",CTy"Random")))
520 Call("rec'Random",CTy"Random",Var("x",F32)))
535 Call("reg'Wired",F32,Var("x",CTy"Wired")))
539 Call("rec'Wired",CTy"Wired",Var("x",F32)))
558 Call("reg'PageMask",F32,Var("x",CTy"PageMask")))
562 Call("re
946 CC[LS"MIPS exception ",Call("hex",sTy,Var("ExceptionCode",FTy 5))]) exception
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscvScript.sml | 401 (Call
403 Call
455 (Call
457 Call
560 (Call
562 Call
614 Call("reg'mcpuid",F64,Var("x",CTy"mcpuid")))
618 Call("rec'mcpuid",CTy"mcpuid",Var("x",F64)))
634 Call("reg'mimpid",F64,Var("x",CTy"mimpid")))
638 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0Script.sml | 159 Call("reg'PRIMASK",F32,Var("x",CTy"PRIMASK")))
163 Call("rec'PRIMASK",CTy"PRIMASK",Var("x",F32)))
188 Call("reg'PSR",F32,Var("x",CTy"PSR")))
192 Call("rec'PSR",CTy"PSR",Var("x",F32)))
209 Call("reg'CONTROL",FTy 3,Var("x",CTy"CONTROL")))
213 Call("rec'CONTROL",CTy"CONTROL",Var("x",FTy 3)))
237 Call("reg'AIRCR",F32,Var("x",CTy"AIRCR")))
241 Call("rec'AIRCR",CTy"AIRCR",Var("x",F32)))
264 Call("reg'CCR",F32,Var("x",CTy"CCR")))
268 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/ |
| H A D | mipsScript.sml | 330 Call("reg'Index",F32,Var("x",CTy"Index")))
334 Call("rec'Index",CTy"Index",Var("x",F32)))
349 Call("reg'Random",F32,Var("x",CTy"Random")))
353 Call("rec'Random",CTy"Random",Var("x",F32)))
368 Call("reg'Wired",F32,Var("x",CTy"Wired")))
372 Call("rec'Wired",CTy"Wired",Var("x",F32)))
392 Call("reg'EntryLo",F64,Var("x",CTy"EntryLo")))
396 Call("rec'EntryLo",CTy"EntryLo",Var("x",F64)))
415 Call("reg'PageMask",F32,Var("x",CTy"PageMask")))
419 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/monadic-arm/ |
| H A D | armScript.sml | 409 MB(Call("ArchVersion",ATy(qTy,PTy(nTy,qTy)),LU),
452 MB(Call("ArchVersion",ATy(qTy,PTy(nTy,qTy)),LU),
527 Call("reg'PSR",F32,Var("x",CTy"PSR")))
531 Call("rec'PSR",CTy"PSR",Var("x",F32)))
612 Call("reg'SCTLR",F32,Var("x",CTy"SCTLR")))
616 Call("rec'SCTLR",CTy"SCTLR",Var("x",F32)))
699 Call("reg'HSCTLR",F32,Var("x",CTy"HSCTLR")))
703 Call("rec'HSCTLR",CTy"HSCTLR",Var("x",F32)))
753 Call("reg'HSR",F32,Var("x",CTy"HSR")))
757 Call("re
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8Script.sml | 406 Call("reg'TCR_EL1",F64,Var("x",CTy"TCR_EL1")))
410 Call("rec'TCR_EL1",CTy"TCR_EL1",Var("x",F64)))
429 Call("reg'TCR_EL2_EL3",F32,Var("x",CTy"TCR_EL2_EL3")))
433 Call("rec'TCR_EL2_EL3",CTy"TCR_EL2_EL3",Var("x",F32)))
461 Call("reg'SCTLRType",F32,Var("x",CTy"SCTLRType")))
465 Call("rec'SCTLRType",CTy"SCTLRType",Var("x",F32)))
544 (Call
603 EQ(Var("w",BTy"N"),Call("Align",BTy"N",TP[Var("w",BTy"N"),nVar"n"])))
618 Call
623 (Call
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | DragDrop.sml | 35 (* Call DragAcceptFiles to accept files. *)
38 (* Call DragFinish when finished processing a WM_DROP message. *)
41 (* Call DragQueryFile to get the file(s). *)
65 (* Call DragQueryPoint to find out where to drop the file(s). *)
|
| H A D | Metafile.sml | 127 (* Call with a NULL buffer to find out how big it is. *)
143 (* Call with a NULL buffer to find out how big it is. *)
159 (* Call with a NULL buffer to find out how big it is. *)
196 (* Call with a null pointer to get the size. *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/s390/ |
| H A D | sysv.S | 66 basr %r14,%r4 # Call ffi_prep_args
137 bas %r14,0(%r12,%r13) # Call helper
267 basr %r14,%r4 # Call ffi_prep_args
340 brasl %r14,ffi_closure_helper_SYSV # Call helper
|
| /seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
| H A D | pars_skl.py | 54 call = lhs_pars.Call()
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/m68k/ |
| H A D | sysv.S | 70 | Call ffi_prep_args
87 | Call the function
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/vax/ |
| H A D | elfbsd.S | 51 # Call ffi_prep_args
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arm/ |
| H A D | sysv.S | 57 Function Call Guide */
174 @ Call ffi_prep_args(stack, &ecif)
351 @ Call ffi_prep_args(stack, &ecif, vfp_space)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
| H A D | X86FOREIGNCALL.sml | 187 CallFunction(DirectReg entryPtrReg), (* Call the function *)
286 CallFunction(DirectReg entryPtrReg), (* Call the function *)
362 CallFunction(DirectReg entryPtrReg), (* Call the function *)
452 CallFunction(DirectReg entryPtrReg), (* Call the function *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/alpha/ |
| H A D | osf.S | 160 # Call ffi_closure_osf_inner to do the bulk of the work.
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 101 val pat = ``Call next name args strs``
305 in commas [int_to_hex n,"Call",
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/metag/ |
| H A D | sysv.S | 133 ! Call ffi_prep_args(stack, &ecif)
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/pa/ |
| H A D | hpux32.S | 86 /* Call prep_args:
107 bl $$dyncall, %r31 ; Call the user function
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/sparc/ |
| H A D | v8.S | 209 ! Call ffi_closure_sparc_inner to do the bulk of the work.
|
| H A D | v9.S | 176 ! Call ffi_closure_sparc_inner to do the bulk of the work.
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sig | 212 val Call : string * ParseDatatype.pretype * Term.term -> Term.term value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Tactical.sml | 525 * Call a thm-tactic for every assumption.
531 * Call a thm-tactic for the first assumption at which it succeeds.
554 * Call a thm-tactic for the first assumption at which it succeeds and
641 * Call a thm-tactic on the "assumption" obtained by negating the goal, i.e.,
|
| /seL4-l4v-10.1.1/HOL4/src/boss/ |
| H A D | bossLib.sig | 114 (* Call-by-value evaluation *)
|