/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | jiraver439.c | 35 static unsigned xx = 1; local 36 return xx; 47 static unsigned xx = 0; local 48 xx += x; 49 return xx;
|
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/parse-tests/ |
H A D | loop_test.c | 22 uint *xx = &moop; local 26 *xx = 3;
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | selftest.sml | 170 val _ = app (ignore o hide) ["aa", "bb", "xx", "pp", "qq"] 172 val g = ([] : term list, ``case xx of (aa,bb) => aa /\ bb``) 176 aconv a ``xx = (aa:bool,bb:bool)`` 182 val a = ``case xx of (aa,bb) => aa /\ bb`` 188 aconv a1 ``xx = (aa:bool, bb:bool)`` andalso
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | cheney_gcScript.sml | 84 roots_inv (b,j,m,xx) = 85 ?v. (v o v = I) /\ (xx = apply v (abs m)) /\ 90 cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) = 106 roots_inv (b,j,m,abs xx) (* memory is permuted *)`; 145 ``cheney_inv(b,b',i,j,j',e,f,m,x,xx,r) /\ ~(i = j) ==> ?ax ay ad. m i = DATA (ax,ay,ad)``, 234 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ (m x = DATA (n',n'',d')) /\ (m j = EMP) ==> 295 cheney_inv (b,b',i,j,j',e,f,m,w,xx,r) /\ IRANGE (b,e) x /\ ~(x = 0) ==> 325 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ ~(j = e) /\ IRANGE(b,e)x ==> 339 ``cheney_inv (b,b',i,j,j3,e,f,m,w,xx,r) /\ {x} SUBSET0 DR0(ICUT(b,e)m) ==> 341 cheney_inv(b,b',i,j2,j3,e,f,m2,w,xx, [all...] |
H A D | arm_cheney_gcScript.sml | 337 ``!a b b' i j j2 j3 e m m2 w ww r x xj2 xx2 xs xs2 d x2 xx r7 r8 r7_2 r8_2 d2. 370 ``ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\ ~(i = j) /\ 373 ref_cheney_inv (b,i',j',j',e',f,m',x,xx,r) (a,r3',r4',d,xs',ys) /\ (d = d') /\ 376 \\ `cheney_inv (b,b,i',j',j',e',f,m',x,xx,r)` by METIS_TAC [cheney_inv_step] 419 Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j2`,`j`,`e`,`m`,`m2`,`x`,`xx`,`r`,`ax`,`r41`,`r52`,`xs`,`xs1`,`d`,`x2`,`ad`,`r7`,`r8`,`r71`,`r81`,`d1`]) ref_cheney_move 423 Q.SPECL [`a`,`b`,`b`,`i`,`j2`,`j3`,`j`,`e`,`m2`,`m3`,`x`,`xx`,`r`,`ay`,`r42`,`r62`,`xs1`,`xs2`,`d1`,`y3`,`ad1`,`r71`,`r81`,`r72`,`r82`,`d2`]) ref_cheney_move 425 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bb` (K ALL_TAC)) 426 \\ REPEAT (Q.PAT_X_ASSUM `ccc ==> !xx.bb` (K ALL_TAC)) 457 ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\ 460 ref_cheney_inv (b,i',i',i',e,f,m',x,xx, [all...] |
H A D | lisp_gcScript.sml | 167 ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e ==> ~(ref_field a (x,xx) = 0w)``, 169 \\ Cases_on `xx` \\ Cases_on `r` 267 (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==> 268 ref_cheney (m1,e) (a,d,xs2,ys) /\ (x2 = ref_field a (x1,xx)) /\ (j2 = ref_addr a j1) /\ (d2 = d) /\ 269 arm_move_pre(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs)``, 275 THEN1 (Cases_on `xx` \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 337 ``!a b b' i j j2 j3 e m m2 w ww r x xj2 xx2 xs xs2 d x2 xx r7 r8 r7_2 r8_2 d2. 340 (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs) = (xj2,xx2,r7_2,r8_2,d2,xs2)) ==> 344 (ref_field a (x2,xx) = xx2) /\ (ref_addr a j2 = xj2) /\ (d = d2) /\ 345 arm_move_pre(ref_addr a j,ref_field a (x,xx), r [all...] |
H A D | improved_gcScript.sml | 691 \\ Q.PAT_X_ASSUM `move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [move_def] 698 \\ Q.PAT_X_ASSUM `move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [move_def] 746 \\ REPEAT (Q.PAT_X_ASSUM `~(RANGE(xx,yy)df)` (K ALL_TAC)) 772 \\ `!xx. z UNION xx UNION {n} = z UNION {n} UNION xx` by SET_TAC 1094 \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC
|
H A D | arm_improved_gcScript.sml | 456 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz. bb` (K ALL_TAC)) 531 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_list","move_list","gc_inv"]) 584 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_roots","move_list","gc_inv"]) 635 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz dd. bb` (K ALL_TAC)) 641 \\ Q.PAT_X_ASSUM `xx = (i2,m2)` MP_TAC 861 \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | huge_struct.c | 66 int8_t xx; member in struct:BigStruct 152 retVal.qq, retVal.rr, retVal.ss, retVal.tt, retVal.uu, (unsigned long)retVal.vv, retVal.ww, retVal.xx); 311 retVal.qq, retVal.rr, retVal.ss, retVal.tt, retVal.uu, (unsigned long)retVal.vv, retVal.ww, retVal.xx); 339 retVal.qq, retVal.rr, retVal.ss, retVal.tt, retVal.uu, (unsigned long)retVal.vv, retVal.ww, retVal.xx);
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_equalScript.sml | 553 ``!x1 a. ~(xx IN b) /\ ~(xx - 4w IN b) ==> 554 (lisp_x x1 (a,b,(xx =+ x) f) s = lisp_x x1 (a,b,f) s)``, 557 \\ `~(xx = a)` by METIS_TAC [] 559 \\ `~(a = xx - 4w)` by METIS_TAC [] 567 \\ Q.PAT_ABBREV_TAC `xx = a - n2w n` 568 \\ `~(xx IN bb) /\ ~(xx - 4w IN bb)` by 569 (Q.UNABBREV_TAC `bb` \\ Q.UNABBREV_TAC `xx` 583 (Q.UNABBREV_TAC `xx` [all...] |
H A D | lisp_parseScript.sml | 1083 \\ Q.PAT_X_ASSUM `!xx. bb ==> bbb` (ASSUME_TAC o Q.SPEC `STRLEN t2`) 1085 \\ Q.PAT_X_ASSUM `!xx. bb` (ASSUME_TAC o RW [] o Q.SPEC `t2`) 1776 (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`]) 1778 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1802 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`]) 1804 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1865 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`3w`,`r4`]) 1867 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1921 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r4`,`y''''`]) 1923 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx y [all...] |
H A D | lisp_proofScript.sml | 24 (x2sexp (F,xx,FunCon s) = Sym s) /\ 25 (x2sexp (F,xx,FunVar s) = Sym s) /\ 26 (x2sexp (F,xx,Lambda vs x) = 28 (x2sexp (F,xx,Label l f) = list2sexp [Sym "label"; Sym l; x2sexp (F,Var "nil",f)]) /\ 58 val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_equalScript.sml | 85 (lisp_equal_stack [] xx yy zz = T) /\ 252 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 254 \\ IMP_RES_TAC lisp_inv_car \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 264 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC)) 266 \\ IMP_RES_TAC lisp_inv_cdr \\ REPEAT (Q.PAT_X_ASSUM `!xs xx xxxx. bbb` (K ALL_TAC))
|
H A D | lisp_bytecode_stepScript.sml | 525 REPEAT STRIP_TAC \\ CCONTR_TAC \\ Q.PAT_X_ASSUM `xx = yy` MP_TAC 637 \\ Q.PAT_X_ASSUM `!xx.bbb` (MP_TAC o Q.SPECL [`n`,`p1`]) 672 ?xx. (one_byte_list (w1 + n2w p1) (bc_ref (p1,sym) x) * xx) (fun2set (d,dd))``, 705 \\ Q.PAT_X_ASSUM `!xx.bb` (MP_TAC o Q.SPECL [`INIT_SYMBOLS ++ sym`,`SOME (dd,d)`]) 718 \\ Q.SPEC_TAC (`xx`,`res`) 1106 \\ REVERSE (Cases_on `?xx. bc1.code p1 = SOME xx`) THEN1 1115 \\ `bc_ref (p1,syms) xx = bc_ref (p1,syms) (THE (bc1.code p1))` by
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_codegenScript.sml | 408 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 415 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 422 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 429 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 443 \\ Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 482 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 508 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 535 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 567 \\ Q.PAT_ASSUM `!xx.bb` (K ALL_TAC)
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/typing/ |
H A D | sttVariantsScript.sml | 144 Q.MATCH_ABBREV_TAC `P GG (LAM vv MM) (A --> B) xx` THEN 145 Q_TAC (NEW_TAC "z") `{vv} UNION FV MM UNION ctxtFV GG UNION fv xx` THEN
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_execScript.sml | 1081 \\ Q.PAT_X_ASSUM `MR_evl (MAP term2term (MAP SND ts),a,xx) bb` MP_TAC 1234 \\ Q.PAT_X_ASSUM `!x1 x2 x3 x4 x5. bbb ==> MR_ev (Or xx,yyy) zz` MATCH_MP_TAC 1259 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1295 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC 1301 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC 1316 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC 1551 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1570 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1592 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1633 \\ REPEAT (Q.PAT_X_ASSUM `!xx [all...] |
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsTools.sml | 407 val (xx,yy) = vc_asms fvL0 (t::(rev asm)) value 409 (hd xx, tl xx, hd yy, tl yy)
|
H A D | quantHeuristicsLibAbbrev.sml | 200 val q = `f (_, xx)`
|
/seL4-l4v-10.1.1/HOL4/examples/miller/miller/ |
H A D | miller_rabinScript.sml | 523 >> Q.PAT_X_ASSUM `xx = n` (AR_TAC o wrap o SYM) 626 >> Q.PAT_X_ASSUM `xx:num = 1` MP_TAC 733 >> Q.PAT_X_ASSUM `gpow xx v k = yy` MP_TAC
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 172 PMATCH_ROW (\ ((xx :bool),(yy :bool list)). (SOME xx,yy)) 173 (\ ((xx :bool),(yy :bool list)). T) 174 (\ ((xx :bool),(yy :bool list)). 3n); 652 val _ = test_conv "PMATCH_REMOVE_DOUBLE_BIND_CONV" PMATCH_REMOVE_DOUBLE_BIND_CONV (``case (xx:('a # 'a)) of (x, x) => T | _ => F``, SOME ``case (xx:('a # 'a)) of (x, x') when (x' = x) => T | _ => F``) ;
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/ |
H A D | stop_and_copyScript.sml | 709 \\ Q.PAT_X_ASSUM `rel_move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [rel_move_def] 717 \\ Q.PAT_X_ASSUM `rel_move xx = fg` MP_TAC \\ ASM_SIMP_TAC (srw_ss()) [rel_move_def] 768 \\ REPEAT (Q.PAT_X_ASSUM `~(RANGE(xx,yy)df)` (K ALL_TAC)) 794 \\ `!xx. z UNION xx UNION {n} = z UNION {n} UNION xx` by SET_TAC 1127 \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/multiword/ |
H A D | multiwordScript.sml | 1108 \\ Q.PAT_X_ASSUM `!xx.bb` (MP_TAC o Q.SPEC `t`) 1738 qpat_x_assum `mw2n (REVERSE xx) = yy` (K ALL_TAC) >> 1752 qpat_x_assum `mw2n (REVERSE xx) = yy` (K ALL_TAC) >> 2000 `!xx yy.MIN xx yy <= yy` by srw_tac[][] >> 2001 `q' <= b - 1` by METIS_TAC[] >> qpat_x_assum `!xx yy. zzz` (fn x => ALL_TAC) >> 2089 qpat_x_assum `xx DIV X2 = A` (fn x => REWRITE_TAC[x]) >> 2302 qpat_x_assum ` xx /\ (us = us) /\ yyy ==> zz` (K ALL_TAC) >> 2308 qpat_x_assum `mw2n (FRONT xx) = mw2n xx` (f [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | whileScript.sml | 406 THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
H A D | chap3Script.sml | 804 `?xx. y =b=> xx /\ x' =b=> xx` by PROVE_TAC [] THEN
|