/seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
H A D | jiraver254.c | 13 int g(_Bool b2) argument 15 return b2 > 3;
|
H A D | parse_addr.c | 19 int b2[10][10]; variable 33 int z = *f(b2[3]);
|
/seL4-l4v-master/HOL4/src/bag/ |
H A D | selftest.sml | 5 ���b5 + (b1: 'a bag) + b2 + b4 - (b2 + b1)���, 8 ���b5 + (b1: 'a bag) + b2 + b4 = b2 + b6 + b1���, ���(b4:'a bag) + b5 = b6���), 10 ���SUB_BAG b2 (b5 + (b1: 'a bag) + b2 + b4)���, ���{||} <= b1 + b4 + b5���)
|
H A D | bagScript.sml | 32 `SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2`); 36 `PSUB_BAG b1 b2 <=> SUB_BAG b1 b2 /\ ~(b1 = b2)`); 61 ``BAG_DIFF b1 (b2:'a bag) = \x. b1 x - b2 x``); 87 `BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2 [all...] |
H A D | primeFactorScript.sml | 96 (* can show p divides BAG_PROD b2, so p is also in b2 (because p is prime). *) 97 (* Let b1' = b1-p and b2' = b2-p. Then b1' = b2', by induction hypothesis. *) 98 (* Thus b1=b2. The argument uses a lemma derived from gcdTheory.P_EUCLIDES, *) 104 ``!n b1 b2. 106 (FINITE_BAG b2 /\ (!m. BAG_IN m b2 ==> prime m) /\ (n=BAG_GEN_PROD b2 [all...] |
H A D | bagSimpleLib.sml | 118 val (b1,b2) = dest_union b; 120 val t2 = mk_image (f, b2) 125 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION)) 127 val bag_thm' = MP (ISPECL [b1,b2,f] bagTheory.BAG_IMAGE_FINITE_UNION) finite_thm12 182 val (b1,b2) = dest_union b; 184 val (finite_thm2, card_thm2) = BAG_CARD_CONV___FINITE b2; 187 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION)) 189 val card_thm' = MP (ISPECL [b1,b2] bagTheory.BAG_CARD_UNION) finite_thm12 284 fun get_resort_lists___pred_pair p b1 b2 = 287 val l2 = fst (strip_insert b2); [all...] |
/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | mod16Script.sml | 79 val MOD16_PROJ_def = Define `MOD16_PROJ (b3,b2,b1,b0) i = if i = 0 then b0 else if i=1 then b1 else if i=2 then b2 else b3` 82 `MOD16_N2B' n k (b3,b2,b1,b0) = 85 else (if n >= 2**k then MOD16_PROJ (b3,b2,b1,b0) k else ~(MOD16_PROJ (b3,b2,b1,b0) k)) /\ 86 MOD16_N2B' (if n >= 2**k then n-(2**k) else n) (k-1) (b3,b2,b1,b0)`; 91 val MOD16_N2B_def = Define `MOD16_N2B n (b3,b2,b1,b0) = MOD16_N2B' n 3 (b3,b2,b1,b0)` 93 val MOD16_N2B_15 = save_thm("MOD16_N2B_15",prove(``!b3 b2 b0 b1. MOD16_N2B 15 (b3,b2,b [all...] |
/seL4-l4v-master/HOL4/examples/dev/AES/curried/ |
H A D | MultScript.sml | 41 `xtime (BYTE b7 b6 b5 b4 b3 b2 b1 b0) 43 if b7 then (BYTE b6 b5 b4 (~b3) (~b2) b1 (~b0) T) 44 else (BYTE b6 b5 b4 b3 b2 b1 b0 F)`; 62 `b1 ** b2 = 65 then b2 # (RightShift b1 ** xtime b2) 66 else (RightShift b1 ** xtime b2)`, 90 `IterConstMult (b1,b2,acc) = 91 if b1 = ZERO then (b1,b2,acc) 92 else IterConstMult (RightShift b1, xtime b2, [all...] |
H A D | word8Script.sml | 32 `(!x:word8. P x) = !b7 b6 b5 b4 b3 b2 b1 b0. P(BYTE b7 b6 b5 b4 b3 b2 b1 b0)`, 139 `BYTE_TO_NUM (BYTE b7 b6 b5 b4 b3 b2 b1 b0) = 141 16*B2N(b4) + 8*B2N(b3) + 4*B2N(b2) + 2*B2N(b1) + B2N(b0)`; 173 `LeftShift (BYTE b7 b6 b5 b4 b3 b2 b1 b0) = BYTE b6 b5 b4 b3 b2 b1 b0 F`; 176 `RightShift (BYTE b7 b6 b5 b4 b3 b2 b1 b0) = BYTE F b7 b6 b5 b4 b3 b2 b1`; 184 of (BYTE b7 b6 b5 b4 b3 b2 b1 b0) -> BYTE b6 b5 b4 b3 b2 b [all...] |
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/ |
H A D | MultScript.sml | 41 `xtime ((b7,b6,b5,b4,b3,b2,b1,b0) :word8) 43 if b7 then (b6,b5,b4,~b3,~b2,b1,~b0,T) 44 else (b6,b5,b4,b3,b2,b1,b0,F)`; 62 `b1 ** b2 = 65 then b2 # (RightShift b1 ** xtime b2) 66 else (RightShift b1 ** xtime b2)`, 91 `IterConstMult (b1,b2,acc) = 92 if b1 = ZERO then (b1,b2,acc) 93 else IterConstMult (RightShift b1, xtime b2, [all...] |
H A D | word8Script.sml | 29 `(!x:word8. P x) = !b7 b6 b5 b4 b3 b2 b1 b0. P(b7,b6,b5,b4,b3,b2,b1,b0)`, 133 `BYTE_TO_NUM (b7,b6,b5,b4,b3,b2,b1,b0) = 135 16*B2N(b4) + 8*B2N(b3) + 4*B2N(b2) + 2*B2N(b1) + B2N(b0)`; 167 `LeftShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (b6,b5,b4,b3,b2,b1,b0,F)`; 170 `RightShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (F,b7,b6,b5,b4,b3,b2,b1)`; 188 (b7,b6,b5,b4,b3,b2,b1,b0) = 199 (case BIT_COMPARE a2 b2 [all...] |
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/ |
H A D | translationsLibScript.sml | 63 (* |- !b1 b2 DS l pf. 65 (l,b1,b2,pf) IN DS.B ==> 68 ((LTL_NOT l,b2,b1,(\sv. P_NOT (pf sv))) INSERT DS.B)) 175 (prove (``!b1 b2 p. 178 {(LTL_PROP p,b1,b2,(\sv. p))} (P_USED_VARS p))``, 185 !b1 b2 DS l pf. 187 (DS.B = {(l,b2,b1,pf)}) ==> 190 {(LTL_NOT l,b1,b2,(\sv. P_NOT (pf sv)))})``, 194 Q_SPECL_NO_ASSUM 0 [`b2`, `b1`, `DS`, `l`, `pf`] THEN 207 !b1 b2 DS [all...] |
H A D | translationsLib.sml | 72 fun getBindingFor b1 b2 l [] = (false, false, ``dummy:num``) 73 | getBindingFor b1 b2 l (h::l1) = 78 if ((l' ~~ l) andalso ((not b1) orelse a1) andalso ((not b2) orelse a2)) then 81 getBindingFor b1 b2 l l1 178 fun ltl2omega_internal2 b1 b2 l dsThm TSPECL = 189 fun addBindingFor b1 b2 l dsThm = 192 val (b1', b2', pf) = getBindingFor b1 b2 l dsB; 194 if (b1' orelse b2') then (b1', b2', p [all...] |
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | xprop_logicScript.sml | 38 (XP_USED_CURRENT_VARS (XP_AND(b1,b2)) = 39 (XP_USED_CURRENT_VARS b1) UNION (XP_USED_CURRENT_VARS b2))`; 46 (XP_USED_X_VARS (XP_AND(b1,b2)) = (XP_USED_X_VARS b1) UNION (XP_USED_X_VARS b2))`; 56 (XP_VAR_RENAMING f (XP_AND(b1,b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2))`; 68 (XP_SEM (XP_AND (b1,b2)) (s1, s2) = ((XP_SEM b1 (s1, s2)) /\ (XP_SEM b2 (s1, s2))))`; 81 `XP_OR(b1, b2) = XP_NOT(XP_AND(XP_NOT b1, XP_NOT b2))`; [all...] |
H A D | prop_logicScript.sml | 39 (P_SEM s (P_AND(b1,b2)) = (P_SEM s b1 /\ P_SEM s b2))`; 49 `P_OR (b1, b2) = P_NOT (P_AND (P_NOT b1, P_NOT b2))`; 52 `P_IMPL (b1, b2) = P_OR (P_NOT b1, b2)`; 55 `P_COND (c, b1, b2) = P_AND (P_IMPL (c, b1), P_IMPL (P_NOT c, b2))`; 58 `P_EQUIV (b1, b2) = P_AND (P_IMPL (b1, b2), P_IMP [all...] |
/seL4-l4v-master/HOL4/examples/hfs/ |
H A D | hfbScript.sml | 10 (���x1 x2 b1 b2. 11 hfb0_equiv x1 x2 ��� hfb0_equiv b1 b2 ��� 12 hfb0_equiv (HF_I x1 b1) (HF_I x2 b2)) ���
|
/seL4-l4v-master/HOL4/src/new-datatype/ |
H A D | NDSupportScript.sml | 22 /\ (sum_retrieve _ f2 (INR a2) (_, b2) = f2 a2 b2)`; 26 /\ (prod_retrieve _ f2 (_, a2) (INR b2) = f2 a2 b2)`;
|
/seL4-l4v-master/HOL4/examples/dev/AES/word8/ |
H A D | MultScript.sml | 45 `b1 ** b2 = 48 then b2 ?? ((b1 >>> 1) ** xtime b2) 49 else ((b1 >>> 1) ** xtime b2)`, 70 `IterConstMult (b1,b2,acc) = 71 if b1 = 0w:word8 then (b1,b2,acc) 72 else IterConstMult (b1 >>> 1, xtime b2, 73 if word_lsb b1 then (b2 ?? acc) else acc)`; 89 `!b1 b2 acc. (b1 ** b2) [all...] |
/seL4-l4v-master/HOL4/examples/Crypto/AES/ |
H A D | MultScript.sml | 44 `b1 ** b2 = 47 then b2 ?? ((b1 >>> 1) ** xtime b2) 48 else ((b1 >>> 1) ** xtime b2)`; 66 `IterConstMult (b1,b2,acc) = 67 if b1 = 0w:word8 then (b1,b2,acc) 68 else IterConstMult (b1 >>> 1, xtime b2, 69 if word_lsb b1 then (b2 ?? acc) else acc)`; 79 `!b1 b2 acc. (b1 ** b2) [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 [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 42 val (a2,b2) = dest_pair rha; 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) 64 val (a2,b2) 553 val b2 = ``& ^b2x + 1i``; value [all...] |
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | Norm_ineqs.sml | 102 (let val (c,b1,b2) = 104 in if (coeff1 = coeff2) then ((name1,coeff1)::c,b1,b2) 106 ((name1,coeff1)::c,b1,(name1,coeff2 - coeff1)::b2) 109 b2) 112 (let val (c,b1,b2) = 114 in (c,(name1,coeff1)::b1,b2) 116 else (let val (c,b1,b2) = 118 in (c,b1,(name2,coeff2)::b2)
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | dataabs.ml | 89 "!n b1 b2. 91 isBus n b2 93 !t1 t2. (b1 t1 = b2 t2) = (!m. m <= n ==> (b1 t1 m = b2 t2 m))",
|
H A D | toplevel.ml | 39 ?phiA w1 b1 b2. 42 DISPLAY n (phiA,b2,display) /\ 43 COUNT_IMP n (phiA,w1,b1,b2) /\ 45 isBus n b2");; 90 WordVal n(WordAbs((b2 when (isHi phiA))((n' + sysinit) + 1)))";;
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_improved_gcScript.sml | 188 ``~(RANGE (b2,e2) j) ==> 189 (ref_mem ((j =+ x) m) b2 e2 = ref_mem m b2 e2)``, 190 completeInduct_on `e2-b2` \\ REPEAT STRIP_TAC 192 \\ Cases_on `e2<=b2` \\ ASM_SIMP_TAC std_ss [] 193 \\ `~(b2 = j)` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 195 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b2))` 197 \\ `e2 - (b2 + y) < e2 - b2` by DECIDE_TAC 198 \\ `~RANGE (b2 [all...] |