Searched refs:xx (Results 1 - 25 of 57) sorted by relevance

123

/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Djiraver439.c35 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 Dloop_test.c22 uint *xx = &moop; local
26 *xx = 3;
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A Dselftest.sml170 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 Dcheney_gcScript.sml84 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 Darm_cheney_gcScript.sml337 ``!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 Dlisp_gcScript.sml167 ``!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 Dimproved_gcScript.sml691 \\ 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 Darm_improved_gcScript.sml456 \\ 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 Dhuge_struct.c66 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 Dlisp_equalScript.sml553 ``!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 Dlisp_parseScript.sml1083 \\ 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 Dlisp_proofScript.sml24 (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 Dlisp_equalScript.sml85 (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 Dlisp_bytecode_stepScript.sml525 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 Djit_codegenScript.sml408 (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 DsttVariantsScript.sml144 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 Dmilawa_execScript.sml1081 \\ 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 DquantHeuristicsTools.sml407 val (xx,yy) = vc_asms fvL0 (t::(rev asm)) value
409 (hd xx, tl xx, hd yy, tl yy)
H A DquantHeuristicsLibAbbrev.sml200 val q = `f (_, xx)`
/seL4-l4v-10.1.1/HOL4/examples/miller/miller/
H A Dmiller_rabinScript.sml523 >> 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 Dselftest.sml172 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 Dstop_and_copyScript.sml709 \\ 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 DmultiwordScript.sml1108 \\ 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 DwhileScript.sml406 THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
/seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/
H A Dchap3Script.sml804 `?xx. y =b=> xx /\ x' =b=> xx` by PROVE_TAC [] THEN

Completed in 156 milliseconds

123