Searched refs:bb (Results 1 - 25 of 64) sorted by relevance

123

/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Ddot_utils.py81 bb = imm_fun.bbs[bb_n]
82 #print 'BB[%s]: %s' % (bb_n, bb)
83 if len(bb) == 1:
84 n_cap = '0x%x\n' % bb[0]
86 n_cap = '0x%x - 0x%x\n' % (min(bb), max(bb))
88 for n in bb:
93 assert n == bb[0] or i_node.n_edges_to <= 1
95 if not (n == bb[-1] or i_node.nEdgesOut() == 1):
98 assert (n == bb[
[all...]
H A Dconflict.py127 #our context matching assumes that all bb addr has the same n_digits...
472 for bb in ctx:
473 print '%s'% elfFile().addrs_to_f[bb]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/
H A Dibm.sml43 1 bb
48 assert G (aa -> next_event(bb)(cc before dd));
68 VAR bb: boolean;
79 (sat_x1 = 4) & (bb & ((!((!dd) & cc)) & (!dd))): 5 union 6;
82 (sat_x1 = 7) & (bb & ((!((!dd) & cc)) & dd)): 0;
83 (sat_x1 = 8) & (aa & (bb & ((!((!dd) & cc)) & (!dd)))): 9 union 10;
87 DEFINE spec_define_13:= (!spec_define_11) | bb;
88 DEFINE spec_define_10:= (!bb);
90 DEFINE spec_define_0:= (!(((sat_x1 = 6) & ((!((!dd) & cc)) & dd)) | (((sat_x1 = 7) & (bb & ((!((!dd) & cc)) & dd))) | (((sat_x1 = 10) & ((!((!dd) & cc)) & dd)) | ((sat_x1 = 11) & (aa & (bb
[all...]
H A DmodelCheck.sml125 F_WEAK_NEXT_EVENT (B_PROP bb,
H A Dltl2omega.sml122 F_STRONG_NEXT_EVENT (B_PROP bb,
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/proof-tests/
H A Dstruct2.c25 bb(struct word_struct word_struct) { function
86 pp = bb(the_ws);
/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/graph-refine/graph-to-graph/chronos/
H A Demitter.py172 bb = 'startbb'
174 bb = 'contbb'
177 s += ('i %s 4 %s' % (hex(addr),bb))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DtailrecScript.sml38 \\ Q.PAT_X_ASSUM `!kk. (!m. cc) ==> bb`
49 \\ Q.PAT_X_ASSUM `!k. (!m. cc) ==> bb` MATCH_MP_TAC
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_equalScript.sml566 \\ Q.ABBREV_TAC `bb = ch_active_set (a,if u then 1 + limit else 1,i)`
568 \\ `~(xx IN bb) /\ ~(xx - 4w IN bb)` by
569 (Q.UNABBREV_TAC `bb` \\ Q.UNABBREV_TAC `xx`
608 ``(!x. x IN bb \/ x - 4w IN bb ==> (f5 x = ft x)) ==>
609 !t a s. (lisp_x t (a,bb,ft) s = lisp_x t (a,bb,f5) s)``,
677 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. bb` (K ALL_TAC))
727 \\ Q.ABBREV_TAC `bb
[all...]
H A Dlisp_parseScript.sml148 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `bb ==> cc` (K ALL_TAC))
545 Q.PAT_X_ASSUM `!x y. bb` MATCH_MP_TAC \\ Q.EXISTS_TAC `g`
617 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
636 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
1008 \\ Q.PAT_X_ASSUM `!m. bb ==> ccc` (ASSUME_TAC o
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`)
1264 \\ Q.PAT_X_ASSUM `~bb` (K ALL_TAC)
1781 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC)
1814 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/experimental/
H A Dlpc_progScript.sml340 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tReg a (LPC_READ_REG a s1)`)
342 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tStatus a (LPC_READ_STATUS a s1)`)
344 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tRom a (LPC_READ_ROM a s1)`)
346 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tRam a (LPC_READ_RAM a s1)`)
348 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tTime (LPC_READ_TIME s1)`)
350 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tUart0 (LPC_READ_UART0 s1)`)
352 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tUndef (LPC_READ_UNDEF s1)`)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/
H A Dalu.sml66 (* return HOL/CTL truth value corresponding to bit bb of the integer rr. *)
73 fun getbit rr bb l =
75 val b = Option.valOf(Int.fromString bb);
80 fun getctlbit ap_ty rr bb l =
82 val b = Option.valOf(Int.fromString bb);
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/
H A Dhuge_struct.c44 int16_t bb; member in struct:BigStruct
149 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd,
308 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd,
336 retVal.y, retVal.z, retVal.aa, retVal.bb, retVal.cc, retVal.dd,
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/more_theories/
H A DordinalScript.sml1340 `?bb. b + bb = r` by metis_tac [ordle_EXISTS_ADD] >>
1341 `b * d^+ + bb = a` by simp[GSYM ordADD_ASSOC] >>
1361 `?bb. (q = a/b + bb) /\ 0 < bb`
1363 `a = b * (a/b + bb) + r` by metis_tac[] >>
1364 `_ = b * (a/b) + b * bb + r` by metis_tac[ordMULT_LDISTRIB] >>
1365 `a % b = b * bb + r` by metis_tac [ordADD_ASSOC, ordADD_RIGHT_CANCEL] >>
1366 `b * bb
[all...]
/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/machine-code/acl2/
H A Dm1_progScript.sml276 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tPC (pc s1)`)
278 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tLocal a (nth_local a s1)`)
280 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tStack (stack s1)`)
282 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tInstr a (instr a s1)`)
284 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tOK (m1_ok s1)`)
523 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC)
539 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC)
566 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC)
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DwhileScript.sml406 THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
411 THEN Q.PAT_ASSUM `!s1. bb /\ bbb ==> bbbb` MATCH_MP_TAC
/seL4-l4v-10.1.1/HOL4/examples/lambda/cl/
H A DabselimScript.sml357 qmatch_abbrev_tac `aa ��� bb ��� cc` >>
363 full_simp_tac std_ss [Abbr`cc`,Abbr`bb`,(GSYM pred_setTheory.IN_UNION)] >-
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dreorder.c615 static int siftTestCmp(const void *aa, const void *bb) argument
618 const sizePair *b = (sizePair*)bb;
1708 static int varseqCmp(const void *aa, const void *bb) argument
1711 int b = bddvar2level[*((const int*)bb)];
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dprog_x86Script.sml126 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xReg xi yi`)
129 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xStatus xi yi`)
132 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `ei` o Q.SPEC `xEIP ei`)
135 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.GEN `zi` o Q.SPEC `xMem xi yi zi`)
528 \\ Q.PAT_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`])
818 \\ Q.PAT_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`])
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Drealconv.cpp2575 Bigint *bb, *bb1, *bd, *bd0, *bs, *delta; variable
2930 Bfree(bb); variable
3057 bb = d2b(&rv, &bbe, &bbbits); /* rv = bb * 2^bbe */
3124 bb1 = mult(bs, bb);
3125 Bfree(bb); variable
3126 bb = bb1;
3129 bb = lshift(bb, bb2);
3136 delta = diff(bb, b
3569 Bfree(bb); variable
3574 Bfree(bb); variable
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Darm_improved_gcScript.sml245 \\ Q.PAT_X_ASSUM `!a.bb /\ bbbb ==> bbb` (ASSUME_TAC o Q.SPEC `a+1`)
249 \\ Q.PAT_X_ASSUM `bb ==> bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES]
388 \\ Q.PAT_X_ASSUM `!k. bb ==> (m k = H_EMP)` MATCH_MP_TAC \\ RANGE_TAC)
433 \\ REPEAT (Q.PAT_X_ASSUM `~RANGE(bb,ee)ii` (K ALL_TAC))
456 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz. bb` (K ALL_TAC))
635 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz dd. bb` (K ALL_TAC))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dprog_x64Script.sml128 THEN1 (Q.PAT_X_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `zReg xi yi`)
130 THEN1 (Q.PAT_X_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `zStatus xi yi`)
132 THEN1 (Q.PAT_X_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `ei` o Q.SPEC `zRIP ei`)
134 THEN (Q.PAT_X_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.GEN `zi` o Q.SPEC `zMem xi yi zi`)
619 \\ Q.PAT_X_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`])
1097 \\ Q.PAT_X_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`])
1359 (FULL_SIMP_TAC std_ss [SPEC_MOVE_COND] \\ Q.PAT_X_ASSUM `!x.bb` MATCH_MP_TAC
1393 (FULL_SIMP_TAC std_ss [SPEC_MOVE_COND] \\ Q.PAT_X_ASSUM `!x.bb` MATCH_MP_TAC
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_invScript.sml327 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
471 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
550 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
589 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
702 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
783 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
843 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
898 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
946 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC
1149 \\ Q.PAT_X_ASSUM `!x. bb \/ bb
[all...]

Completed in 221 milliseconds

123