/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | ILTheory.sig | 180 (?a0 a1. 182 (\a0 a1. 184 (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\ 185 'CTL_STRUCTURE' a0 /\ 'CTL_STRUCTURE' a1) \/ 186 (?a0 a1 a2. 188 (\a0 a1 a2. 190 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0 a1 a2) /\ 191 'CTL_STRUCTURE' a1 /\ 'CTL_STRUCTUR [all...] |
/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | jiraver443a.c | 16 static int a1; variable 22 return &a1;
|
/seL4-l4v-master/HOL4/examples/STE/Examples/ |
H A D | And.sml | 22 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 25 val A = TF [a1, a2]; 34 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 36 val A = TF [a1]; 44 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 47 val A = TF [a1,a2];
|
H A D | Or.sml | 21 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 24 val A = TF [a1, a2]; 34 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 36 val A = TF [a1]; 47 val a1 = (T, "i0", ``v1:bool``, 0, 1); value 50 val A = TF [a1,a2];
|
H A D | Comparator.sml | 17 else if (node = "a1") then X 22 (Xnor (s "a1")(s "b1")) 29 (s_b' node = (s_b "a0" = s_b "b0") /\ (s_b "a1" = s_b "b1"))`; 49 THEN Cases_on `s_b "a1"` 75 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``) 81 THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"` 96 val a1 = (T, "a1", ``a1 value 116 val a1 = (T, "a1", ``T:bool``, 0, 1); value 136 val a1 = (T, "a1", ``a1:bool``, 0, 1); value 156 val a1 = (T, "a1", ``v1:bool``, 0, 1); value 176 val a1 = (T, "a1", ``T:bool``, 0, 1); value 196 val a1 = (T, "a1", ``F:bool``, 0, 1); value 216 val a1 = (T, "a1", ``F:bool``, 0, 1); value 236 val a1 = (T, "a1", ``F:bool``, 0, 1); value [all...] |
H A D | Comparator-for-STE-Reduction.sml | 27 else if (node = "a1") then X 35 Xnor (s "a1")(s "b1") 40 (Xnor (s "a1")(s "b1")) 56 else if (node = "a1") then X 60 else if (node = "i1") then Xnor (s "a1")(s "b1") 84 val a1 = (T, "a1", ``a1:bool``, 0, 1); value 87 val out = (T, "out", ``xnor a0 b0 /\ xnor a1 b1``, 1, 2); 88 val A = TF [a0,a1,b [all...] |
H A D | Mux.sml | 18 else if (node = "a1") then X 32 (And (s "a1")(s "ctrl")) 45 (s_b' "out1" = s_b "a1") 86 THENL [fl [] THEN Cases_on `s_b "a1"` 92 fl [] THEN Cases_on `s_b "a1"` 124 FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``) 127 THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"` 141 val a1 = (T, "a1", value 166 val a1 = (T, "a1", ``va1:bool``, 0, 1); value 189 val a1 = (T, "a1", ``va1:bool``, 0, 1); value [all...] |
/seL4-l4v-master/HOL4/src/rational/ |
H A D | fracScript.sml | 91 * |- !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==> 92 * ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) ) 99 ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==> 100 ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )``, 125 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 126 * (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2)) 129 val FRAC_NOT_EQ = store_thm("FRAC_NOT_EQ", ``!a1 b [all...] |
H A D | fracLib.sml | 29 * (abs_frac (a1,b1) = abs_frac (a2,b2) 31 * 0<b1, 0<b2 |- (abs_frac (a1,b1) = abs_frac (a1,b1)) 32 * = (a1 = a2) /\ (b1 = b2) : thm 41 val (a1,b1) = dest_pair lha; value 44 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_EQ) 51 * ~((abs_frac (a1,b1) = abs_frac (a2,b2)) 53 * 0<b1, 0<b2 |- ~(abs_frac (a1,b1) = abs_frac (a2,b2)) 54 * = ~(a1 = a2) \/ ~(b1 = b2) 63 val (a1,b value 83 val (a1,b1) = dest_pair lha; value 273 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_nmr_tm end) value 277 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_dnm_tm end) value 550 val (a1,b1) = dest_pair args; value [all...] |
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | infinite_pathScript.sml | 311 ``!t v a1 a2. (EQUIV_ON_PATH_RESTN t v a1 a2) = 312 (IMP_ON_PATH_RESTN t v a1 a2 /\ IMP_ON_PATH_RESTN t v a2 a1)``, 438 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a1 ==> IMP_ON_PATH_RESTN t v a1 a2``, 447 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a2 ==> BEFORE_ON_PATH_RESTN_STRONG t v a1 a2``, 456 ``!v t t2 a1 a [all...] |
H A D | rltlScript.sml | 455 ``!f v a1 a2 r t. (PROP_LOGIC_EQUIVALENT a1 a2) ==> 456 (((RLTL_SEM_TIME t v a1 r f) = (RLTL_SEM_TIME t v a2 r f)) /\ 457 ((RLTL_SEM_TIME t v r a1 f) = (RLTL_SEM_TIME t v r a2 f)))``, 463 `(!s. P_SEM s (P_OR (a1,P_AND (p_2,P_NOT r))) = P_SEM s (P_OR (a2,P_AND (p_2,P_NOT r)))) /\ 464 (!s. P_SEM s (P_OR (r,P_AND (p_2,P_NOT a1))) = P_SEM s (P_OR (r,P_AND (p_2,P_NOT a2))))` 473 ``!f v a1 a2 r1 r2 t. (PROP_LOGIC_EQUIVALENT a1 a2) ==> 475 ((RLTL_SEM_TIME t v a1 r1 f) = (RLTL_SEM_TIME t v a2 r2 f))``, 705 ``!f t v a1 a [all...] |
H A D | automaton_formulaScript.sml | 265 `A_USED_STATE_VARS_COMPATIBLE a1 a2 = 266 (DISJOINT (A_USED_INPUT_VARS a1) (A_USED_STATE_VARS a2) /\ 267 DISJOINT (A_USED_INPUT_VARS a2) (A_USED_STATE_VARS a1) /\ 268 DISJOINT (A_USED_STATE_VARS a1) (A_USED_STATE_VARS a2))`; 272 !a1 a2. VARDISJOINT_AUTOMATON_FORMULA (A_AND(a1, a2)) ==> 273 A_USED_STATE_VARS_COMPATIBLE a1 a2 285 `AUTOMATON_EQUIV a1 a2 = !v. A_SEM v a1 <=> A_SEM v a2`; 290 (!a1 a [all...] |
/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | NDSupportScript.sml | 21 (sum_retrieve f1 _ (INL a1) (b1, _) = f1 a1 b1) 25 (prod_retrieve f1 _ (a1, _) (INL b1) = f1 a1 b1)
|
/seL4-l4v-master/HOL4/examples/lambda/other-models/ |
H A D | diagsScript.sml | 24 (!a1 a2 n b ty. (n, a1, a2, b, ty) IN Fa ==> 25 liftrel b ty (R n) (f a1) (f a2)) ==> 27 (!a1 a2 n b ty. (n, INL a1, INL a2, b, ty) IN G ==> 28 liftrel b ty (R n) (f a1) (f a2)) /\ 249 ?a1 a2. R1 a1 a2 /\ (b1 = f a1) /\ (b2 = f a2) 317 `!n a1 a [all...] |
/seL4-l4v-master/HOL4/src/compute/examples/ |
H A D | Sort.sml | 22 | Tas2Ln (Br (n,a1,a2)) = n::(fusion (Tas2Ln a1) (Tas2Ln a2)) 26 | insTas (Br(m,a1,a2)) n = 27 if (inf_egal n m) then Br(n,a2,insTas a1 m) else Br(m,a2,insTas a1 n)
|
H A D | MergeSort.sml | 51 /\ (Tree2List (Nd n a1 a2) = n :: merge (Tree2List a1) (Tree2List a2)) ` 56 /\ (insTree (Nd m a1 a2) n = 57 if (le_nat n m) then Nd n a2 (insTree a1 m) 58 else Nd m a2 (insTree a1 n)) `
|
/seL4-l4v-master/HOL4/src/combin/ |
H A D | combinpp.sml | 12 fun cAPP l (a1, a2) = Absyn.APP(l,a1,a2) 16 APP(l, a1, a2) => 17 (case a1 of 26 SOME(l, a1, a2) => (a1,a2) 60 | APP(l,a1,a2) => 62 NONE => APP(l, upd_processor G a1, upd_processor G a2)
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/ |
H A D | sbi.h | 54 register register_t a1 asm("a1") = arg_1; 60 : "r"(a0), "r"(a1), "r"(a2), "r"(a7)
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
H A D | registerset.h | 38 a1 = 10, msgInfoRegister = 10, enumerator in enum:_register 143 [seL4_UnknownSyscall_A1] = a1,\ 170 [seL4_TimeoutReply_a1] = a1, \
|
/seL4-l4v-master/seL4/src/arch/riscv/machine/ |
H A D | registerset.c | 29 a0, a1, a2, a3, a4, a5, a6, a7,
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient_sumScript.sml | 59 `(($+++ R1 R2) (INL (a1:'a)) (INL (a2:'a)) = R1 a1 a2) /\ 61 (($+++ R1 R2) (INL a1) (INR b2) = F) /\ 160 !a1 a2. 161 R1 a1 a2 ==> 162 (R1 +++ R2) (INL a1) (INL a2)���), 212 !a1 a2. 213 (R1 +++ R2) a1 a2 ==> 214 (ISL a1 = ISL a2)���), 237 !a1 a [all...] |
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | complex_rationalScript.sml | 67 `COMPLEX_ADD (com a1 b1) (com a2 b2) = 68 com (a1+a2) (b1+b2)`; 80 `COMPLEX_SUB (com a1 b1) (com a2 b2) = 81 com (a1-a2) (b1-b2)`; 93 `COMPLEX_MULT (com a1 b1) (com a2 b2) = 94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | complex_rationalScript.sml | 67 `COMPLEX_ADD (com a1 b1) (com a2 b2) = 68 com (a1+a2) (b1+b2)`; 80 `COMPLEX_SUB (com a1 b1) (com a2 b2) = 81 com (a1-a2) (b1-b2)`; 93 `COMPLEX_MULT (com a1 b1) (com a2 b2) = 94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | complex_rationalScript.sml | 67 `COMPLEX_ADD (com a1 b1) (com a2 b2) = 68 com (a1+a2) (b1+b2)`; 80 `COMPLEX_SUB (com a1 b1) (com a2 b2) = 81 com (a1-a2) (b1-b2)`; 93 `COMPLEX_MULT (com a1 b1) (com a2 b2) = 94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | elliptic_exampleScript.sml | 230 let a1 = ex1_field_elt example1_curve.a1 in 236 let y = ~y1 - a1 * x1 - a3 248 let a1 = ex1_field_elt example1_curve.a1 in 256 let d = & 2 * y1 + a1 * x1 + a3 259 let l = (& 3 * x1 ** 2w + & 2 * a2 * x1 + a4 - a1 * y1) / d in 261 let x = l ** 2w + a1 * l - a2 - &2 * x1 in 262 let y = ~(l + a1) * x - m - a3 276 let a1 [all...] |