Searched defs:r15 (Results 1 - 13 of 13) sorted by relevance

/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_core_decompLib.sml14 val r15 = Term.mk_var ("r15", ``:word32``) value
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/
H A Dtypes.h25 r8, r9, r10, r11, r12, r13, r14, r15; member in struct:seL4_UserContext_
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml122 val r15 = BitsN.fromNat (15, 4) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml125 val r15 = BitsN.fromNat (15, 4) value
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Dselftest.sml118 val r15 = reg 15 value
[all...]
H A Darm_parserLib.sml1559 val r15 = mk_word4 15 value
1593 val r15 = mk_word4 15 value
2202 val r15 = mk_word4 15 value
[all...]
/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/
H A DlemmasScript.sml216 val r15 = SYM (List.nth (CONJUNCTS num2register_thm, 15)) value
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86CODESIG.sml44 and r12: genReg and r13: genReg and r14: genReg and r15: genReg value
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml56 val r15 = mk_var("r15",``:word32``) value
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/prog/
H A Darm8_progLib.sml89 val r15 = stateLib.gvar "pc" dword value
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A Darm_evalScript.sml98 val r15 = SYM (List.nth (CONJUNCTS num2register_thm, 15)) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sml98 val r15 = stateLib.gvar "pc" word value
287 val r15 = wordsSyntax.mk_wordii (15, 4) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_progLib.sml114 val r15 = stateLib.gvar "pc" word value
349 val r15 = wordsSyntax.mk_wordii (15, 4) value

Completed in 203 milliseconds