| /seL4-l4v-master/HOL4/examples/ARM/v4/ |
| H A D | arm_evalLib.sml | 336 let val regs = dest_subst_reg t value
415 let val regs = dest_subst_reg t value
|
| /seL4-l4v-master/HOL4/examples/ARM/v7/ |
| H A D | arm_random_testingLib.sml | 69 val regs = List.map mk_word4 value
|
| H A D | arm_stepLib.sml | 514 val regs = mk_reg_mode_updates (the_state,state') value
|
| H A D | arm_stepScript.sml | 3086 val regs = value
|
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
| H A D | arm_stepScript.sml | 3085 val regs = value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | mechReasoning.sml | |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 6753 val regs = value
6800 val regs = value
26407 val regs = value
26420 val regs = value
26435 val regs = value
26448 val regs = value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/step/ |
| H A D | x64_stepLib.sml | 34 val regs = TypeBase.constructors_of ``:Zreg`` value
|
| /seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
| H A D | reg_allocLib.sml | 346 val regs = map (fn n => mk_var("r" ^ (int_to_string n),``:word32``)) (rev (kk (n-1))) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/ |
| H A D | prog_armLib.sml | 65 val regs = collect_term_of_type ``:word4`` g value
66 val regs = filter wordsSyntax.is_n2w regs value
|
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | prog_ppcLib.sml | 35 val regs = map (fn tm => mk_eq(tm,(snd o process T o cdr o car) tm)) rs value
49 val regs = collect_term_of_type ``:ppc_reg`` g; value
|
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | x86_encodeLib.sml | 82 val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"] value
148 val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"] value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | stateLib.sml | 1616 val regs = List.mapPartial (Lib.total dest_reg) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | stack_analysisLib.sml | 114 val regs = (case !arch_name of value
|
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_compiler_opScript.sml | 2059 val regs = [``x2:SExp``,``x1:SExp``,``x3:SExp``,``x4:SExp``,``x5:SExp``, value
|
| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
| H A D | X86CODESIG.sml | 50 val regs: int value
|
| /seL4-l4v-master/seL4/include/arch/arm/arch/object/ |
| H A D | vcpu.h | 76 word_t regs[seL4_VCPUReg_Num]; member in struct:vcpu
|
| /seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
| H A D | registerset.h | 105 fp_reg_t regs[RISCV_NUM_FP_REGS]; member in struct:user_fpu_state
|
| /seL4-l4v-master/seL4/libsel4/include/sel4/ |
| H A D | deprecated.h | 39 } regs; member in union:__anon177
|
| H A D | faults.h | 75 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_TimeoutReply_new(seL4_Bool resume, seL4_UserContext regs, seL4_Word length) argument
|
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
| H A D | deprecated.h | 45 } regs; member in union:__anon215
62 } regs; member in union:__anon217
|