/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | jiraver434.c | 8 int r2, r3; member in struct:__anon117 14 return ucptr->r2 + ucptr->r3;
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_tests.sml | 5 "e08cc003" (* add ip, ip, r3 *) :: 11 "e283c001" (* add ip, r3, #1 *) :: 12 "e283c002" (* add ip, r3, #2 *) :: 52 "e0800103" (* add r0, r0, r3, lsl #2 *) :: 56 "e2830010" (* add r0, r3, #16 *) :: 57 "e0830200" (* add r0, r3, r0, lsl #4 *) :: 104 "e0811183" (* add r1, r1, r3, lsl #3 *) :: 110 "e2831001" (* add r1, r3, #1 *) :: 111 "e0831101" (* add r1, r3, r1, lsl #2 *) :: 112 "e0831201" (* add r1, r3, r [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | selftest.sml | 106 val r3 = reg 3 value 145 adc pc,r3,r4,asr #29 146 .label: adc sp,r3,r4,lsl lr 154 asr r3,#11 155 asr r3,r9 156 asr r3,r9,r4 157 rrx r3 158 rrx r3,r5 159 ror r3,r5 257 ("LDRBNE r2, [r3]", [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_decomp_demoScript.sml | 18 ed936a00 (* vldr s12, [r3] *) 21 e59d3000 (* ldr r3, [sp] *) 28 edc37a00 (* vstr s15, [r3] *)`; 33 e3003000 (* movw r3, #0 *) 34 e3403000 (* movt r3, #0 *) 35 ed937a00 (* vldr s14, [r3] *) 36 edd37a03 (* vldr s15, [r3, #12] *) 38 edd35a01 (* vldr s11, [r3, #4] *) 39 edd37a05 (* vldr s15, [r3, #20] *) 40 ed936a02 (* vldr s12, [r3, # [all...] |
H A D | arm_core_decompScript.sml | 16 (* r3 *) word32 => 45 (ARM_ASSERTION mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 51 arm_REG (R_mode mode 3w) r3 *
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | divideScript.sml | 24 if_sub(r5:word32,r4:word32,r2:word32,r3:word32) = 27 let r3 = r3 + r2 in 28 (r5,r4,r2,r3) 29 else (r5,r4,r2,r3)`` 32 sub_and_shift(r5:word32,r4:word32,r2:word32,r3:word32) = 33 let (r5,r4,r2,r3) = if_sub (r5,r4,r2,r3) in 35 if r2 = 0w then (r5,r4,r2,r3) else 37 sub_and_shift(r5,r4,r2,r3)``; [all...] |
H A D | lisp_equalScript.sml | 14 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"]; 22 arm_eq_loop (r3:word32,r4:word32,r5:word32,r6:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) = 23 if r3 = r4 then 25 (r3,r4,r5,r6,r7,r8,df,f) 29 let r3 = f (r7 - 0x4w) in 32 arm_eq_loop (r3,r4,r5,r6,r7,r8,df,f) 34 let r5 = r3 || r4 in 36 let r5 = f (r3 + 0x4w) in 37 let r3 = f r3 i [all...] |
H A D | lisp_printScript.sml | 61 arm_string_rev(r3:word32,r6,r7,df:word32 set,f:word32->word8) = 62 if r3 = 0w then (r7,df,f) else 69 let r3 = r3 - 1w in 70 arm_string_rev(r3,r6,r7,df,f)`` 74 let r3 = r7 - r6 in 75 let r3 = r3 >>> 1 in 76 let r6 = r6 + r3 in 78 let r7 = r7 - r3 i [all...] |
H A D | lisp_parseScript.sml | 24 arm_read_loop (r3:word32,r4:word32,r5:word32,df:word32 set,f:word32->word8) = 25 (let r6 = r3 << 2 in 26 let r3 = r3 + r6 in 27 let r3 = r3 + r3 in 28 let r3 = r3 + r4 in 34 (let r4 = r4 + 0x30w in (r3,r [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/compiler/demo/ |
H A D | compiler_demoScript.sml | 54 copy_byte_loop (r3:word32,r4:word32,dg:word32 set,g:word32->word8) = 55 if r3 = 0w then (r3,r4,dg,g) else 56 let r3 = w2w (g r3) in 58 let g = (r4 =+ w2w r3) g in 59 copy_byte_loop (r3,r4,dg,g)``; 88 call_mod10 (r1:word32,r2:word32,r3) = 90 let r1 = r1 + r3 in 100 let r3 [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/test/ |
H A D | tea.sml | 239 (\(r0,r1,r2,r3). 244 let r0 = r0 + r3 in 250 (\((r0,r1),(r2,r3,r4,r5),r6). 252 let r7 = ShiftXor (r1,r6,r2,r3) in 256 ((r0,r1),(r2,r3,r4,r5),r6))) : thm 259 (\(r0,(r1,r2),(r3,r4,r5,r6),r7). 260 (let ((r0,r1),(r2,r3,r4,r5),r6) = 262 ((r1,r2),(r3,r4,r5,r6),r7) 265 let ((r1,r2),(r3,r4,r5,r6),r7) = 266 Round ((r1,r2),(r3,r [all...] |
H A D | refined_format.sml | 12 val (src1,dst1) = (``(r2:word32,r3:word32,r4:word32,r1:word32)``, 13 ``(r1:word32,r2:word32,r3:word32,r4:word32)`` 24 let r2 = atom r3 in 25 let r3 = atom r4 in 27 (r1,r2,r3,r4)) = 28 (r2,r3,r4,r1) : thm 31 val (src2,dst2) = (``(r0:word32,r1:word32,r2:word32,r3:word32)``, 32 ``(r1:word32,r2:word32,r3:word32,r4:word32)`` 45 let r5 = atom r3 in 46 let r3 [all...] |
H A D | CADE_example.sml | 174 (let r3 = r2 + 100 in 176 let r4 = r3 + r4 in 179 r3 183 let r0 = r3 * r0 in 206 ASG (L 1) r3 (r2 + 100) (L 3) |++| 208 (ASG (L 4) r4 (r3 + r4) (L 5) |++| 210 ASG (L 7) r0 r3 (L 6) |++| 213 ASG (L 6) r0 (r3 * r0) (L 2)))),L 2) 214 ((let r3 = r2 + 100 in 216 let r4 = r3 [all...] |
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/ |
H A D | m0_decomp_demoScript.sml | 9 mov r3, r0 ; first address 10 adds r3, #40 ; last address (10 loads) 14 cmp r0, r3 ; test if done
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | ratScript.sml | 1394 |- !r1 r2 r3. r1 < r2 /\ r2 < r3 ==> r1 < r3 1420 ``!r1 r2 r3. rat_les r1 r2 /\ rat_les r2 r3 ==> rat_les r1 r3``, 1423 ``rat_sub r3 r1 = rat_add (rat_sub r3 r2) (rat_sub r2 r1)`` 1431 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r2)`` THEN 1452 |- !r1 r2 r3 [all...] |
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
H A D | types.h | 21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
H A D | types.h | 21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
|
/seL4-l4v-master/HOL4/examples/computability/register/ |
H A D | rmToolsScript.sml | 37 dup0 r1 r2 r3= <| 42 | 3 => Inc r3 (SOME 1) 43 | 4 => Dec r3 (SOME 5) NONE 53 dup r1 r2 r3= <| 59 | 3 => Inc r3 (SOME 1) 60 | 4 => Dec r3 (SOME 5) NONE 409 (dup r1 r2 r3).tf 0 = Dec r2 (SOME 0) (SOME 1) ��� 410 (dup r1 r2 r3).tf 1 = Dec r1 (SOME 2) (SOME 4) ��� 411 (dup r1 r2 r3).tf 2 = Inc r2 (SOME 3) ��� 412 (dup r1 r2 r3) [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | arm_compiler_demoScript.sml | 121 garble (r2:word32,r3:word32,r4:word32) = 122 let r1 = r2 + r3 in 123 let r2 = r1 - r3 << 5 in 124 let r3 = r2 * r3 in 126 let r2 = r3 && r2 >>> 30 in 129 let r3 = r2 !! r1 in 130 let r2 = r3 ?? 55w in 131 (r2,r3)`; 157 f (r1,r2) = let .... in f (r2,r3) [all...] |
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/test/ |
H A D | regexTest.sml | 41 val r3 = Seq (r2, r1); value 56 (19, true, r3, "00011212"), 57 (19, false, r3, "00011213") 89 (101, true, r3, longString ^ "112121212"), 90 (102, false, r3, longString ^ "112121213"),
|
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_incrementalScript.sml | 26 (* assign meanings to r1, r2, r3, r4 etc *) 34 r3 edi - preserved (rest of stack) 176 r3 edi - preserved (rest of stack) 184 r3 - pointer to next code to be generated 213 x86_encodes_jump (r3:word32,r6:word32,df:word32 set,f:word32->word8) = 214 let f = (r3 =+ 0x83w) f in 215 let f = (r3 + 1w =+ 0xF1w) f in 216 let f = (r3 + 2w =+ w2w r6) f in 217 let f = (r3 + 3w =+ 0xFFw) f in 218 let f = (r3 [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | straightlineScript.sml | 12 arm_assert (p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v, 18 arm_REG (R_mode mode 3w) r3 * 50 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v, 52 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v,
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_cheney_gcScript.sml | 19 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"]; 53 E5935000 (* ldr r5,[r3] *) 54 E5936004 (* ldr r6,[r3,#4] *) 57 E4835004 (* L2:str r5,[r3],#4 *) 58 E4836004 (* str r6,[r3],#4 *) 59 E2833004 (* add r3,r3,#4 *)`; 62 E1530004 (* CHENEY:cmp r3,r4 *) 78 E289300C (* add r3,r9,#12 *) (* set i *) 79 00833006 (* addeq r3,r [all...] |
H A D | lisp_gcScript.sml | 16 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"]; 50 E5935000 (* ldr r5,[r3] *) 51 E5936004 (* ldr r6,[r3,#4] *) 54 E4835004 (* L2:str r5,[r3],#4 *) 55 E4836004 (* str r6,[r3],#4 *)`; 58 E1530004 (* CHENEY:cmp r3,r4 *) 74 E2893008 (* add r3,r9,#8 *) (* set i *) 75 00833006 (* addeq r3,r3,r6 *)`; 82 E0835006 (* add r5,r3,r [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/multiword/ |
H A D | mc_multiwordScript.sml | 308 (\(l,r1:'a word,r3:'a word,r8:'a word,r9:'a word,r10:'a word,xs,zs). 312 (INR (l,r1:'a word,r3,r8,r9,r10,xs,zs),T)) 317 let cond = cond /\ (r3 <> 0w ==> (r3 = 1w)) in 318 let (r8,r3) = single_add_word r8 r9 r3 in 323 (INL (l-1,r1,r3,r8,r9,r10,xs,zs),cond /\ l <> 0n)))``; 328 (\(l,r1:'a word,r3:'a word,r8:'a word,r9:'a word,r10:'a word,xs,ys,zs). 332 (INR (l,r1,r3,r8,r9,r10,xs,ys,zs),T)) 339 let cond = cond /\ (r3 <> [all...] |