| /seL4-l4v-10.1.1/seL4/src/arch/arm/32/machine/ |
| H A D | registerset.c | 19 R0, R1, R8, R9, R10, R11, R12
|
| /seL4-l4v-10.1.1/seL4/src/arch/x86/64/machine/ |
| H A D | registerset.c | 18 R10, R8, R9, R15
23 R8, R9, R10, R11, R12, R13, R14, R15
39 context->registers[R8] = 0;
|
| /seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/machine/ |
| H A D | registerset.h | 49 R8 = 10, /* 0x50 */ enumerator in enum:_register
90 [seL4_UnknownSyscall_R8] = R8,\
|
| /seL4-l4v-10.1.1/seL4/include/arch/arm/arch/32/mode/machine/ |
| H A D | registerset.h | 77 R8 = 8, enumerator in enum:_register
115 compile_assert(r8_offset_correct, R8 * sizeof(word_t) == PT_R8)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | ILTheory.sig | 77 val R8 : thm value
1064 || R8 -> v8
1162 [R8] Definition
1164 |- R8 = num2MREG 8
1237 R8
1260 (index_of_reg R6 = 6) /\ (index_of_reg R7 = 7) /\ (index_of_reg R8 = 8) /\
1838 (MREG2num R6 = 6) /\ (MREG2num R7 = 7) /\ (MREG2num R8 = 8) /\
1848 (f R8 = x8) /\ (f R9 = x9) /\ (f R10 = x10) /\ (f R11 = x11) /\
1862 ((M' = R8) ==> (v8 = v8')) /\ ((M' = R9) ==> (v9 = v9')) /\
1875 || R8
[all...] |
| H A D | ILScript.sml | 30 MREG = R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R13 | R14`;
48 (index_of_reg R8 = 8) /\
66 else if i = 8 then R8
84 (from_reg_index 8 = R8) /\
|
| H A D | ILTheory.sml | 395 ("R8",(T"MREG" "IL" [])), ("R7",(T"MREG" "IL" [])),
506 C"R7" "IL" (T"MREG" "IL" []), C"R8" "IL" (T"MREG" "IL" []),
3538 val R8 = DT([], [], `((%11 %28) (%12 (%5 (%22 (%6 (%6 %7))))))`) value
5211 ("R8",R8,DB.Def), ("R9",R9,DB.Def), ("R10",R10,DB.Def),
5348 (temp_overload_on_by_nametype "R8")
5349 {Name = "R8", Thy = "IL"}
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
| H A D | swsepLib.sml | 66 ``mread ^var_old (RR R8)`` |-> ``^var_new (MREG2REG R8)``,
186 ``mread ^var_old (RR R8)`` |-> ``^vals (MREG2REG R8)``,
|
| H A D | swsepScript.sml | 2143 (MREG2REG R8 = 8w) /\
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | Data.sml | 9 | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15;
|
| H A D | armParser.lex | 17 | 8 => R8 | 9 => R9 | 10 => R10 | 11 => R11
|
| H A D | assemblerML.sml | 92 | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | CFLScript.sml | 46 MREG = R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R13 | R14`;
64 (index_of_reg R8 = 8) /\
82 else if i = 8 then R8
100 (from_reg_index 8 = R8) /\
|
| H A D | HSLScript.sml | 121 (conv_reg r5 = R5) /\ (conv_reg r6 = R6) /\ (conv_reg r7 = R7) /\ (conv_reg r8 = R8)`,
|
| H A D | bigInstScript.sml | 279 (* Data registers are restricted to R0-R8 *)
|
| /seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
| H A D | traps.S | 604 push %r8 # save R8 (message register)
645 push %r8 # save R8 (message register)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_Lib.sml | 235 val new_regs = ["R8", "R9", "R10", "R11", "R12", "R13", "R14", "R15"]
307 ("R8" ,"2e52646f7adbc694","2e52646f7adbc694"),
|
| H A D | x64_encodeLib.sml | 106 zip ["R8","R9","R10","R11","R12","R13","R14","R15"] (add_reg_type 64 [8,9,10,11,12,13,14,15]) @
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | ILScript.sml | 30 MREG = R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R13 | R14`;
48 (index_of_reg R8 = 8) /\
66 else if i = 8 then R8
84 (from_reg_index 8 = R8) /\
|
| /seL4-l4v-10.1.1/HOL4/src/meson/test/ |
| H A D | selftest.sml | 3084 (!P8 R8 Q8. equal(P8,Q8) ==> equal(f8(R8,P8),f8(R8,Q8))) /\
|