| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | check.py | 23 from syntax import (true_term, false_term, boolT, mk_var, mk_word32, mk_word8, namespace
688 ret_eq = eq_hyp ((true_term, (('Ret', restrs), l_tag)),
689 (true_term, (('Ret', restrs), r_tag)))
|
| H A D | debug.py | 110 cond = m[name] == syntax.true_term
120 == syntax.true_term]
155 assert r in [syntax.true_term, syntax.false_term], r
156 return r == syntax.true_term
369 assert v in [syntax.true_term, syntax.false_term]
859 return rep_graph.eq_hyp ((expr, vis), (syntax.true_term, vis))
|
| H A D | inst_logic.py | 99 (syntax.true_term, 'C_IN')) for (nm, typ) in bin_globs]
103 (syntax.true_term, 'C_OUT')) for (nm, typ) in bin_globs]
|
| H A D | logic.py | 11 from syntax import true_term, false_term, mk_num namespace
75 ((mk_rodata (c_imem), c_in), (true_term, c_in))]
77 ieqs = [((mk_rodata (a_imem), a_in), (true_term, c_in))]
82 ((mk_rodata (c_omem), c_out), (true_term, c_out))]
186 preconds = [((a_x, 'ASM_IN'), (true_term, 'ASM_IN')) for a_x in preconds]
472 return true_term
638 if node.kind == 'Cond' and node.cond == true_term:
1026 % (n2, c == syntax.true_term))
1027 if c == syntax.true_term:
1611 if vals[1] in [syntax.true_term, synta
[all...] |
| H A D | loop_bounds.py | 6 from syntax import mk_not, true_term, false_term, mk_implies, Expr, Type, unspecified_precond_term,mk_and namespace
|
| H A D | problem.py | 9 from syntax import (Expr, mk_var, Node, true_term, false_term, namespace
702 true_term, false_term]:
|
| H A D | rep_graph.py | 10 from syntax import (true_term, false_term, boolT, mk_and, mk_not, mk_implies, namespace
206 if pc[0] == 'Bool' and pc[1] == true_term:
257 return syntax.true_term
284 return Hyp ('EqIfAt', (expr, vis), (true_term, vis),
289 return Hyp ('PCImp', ('Bool', true_term), vis)
528 return (true_term, self.inp_envs[n])
666 elif node.kind == 'Cond' and node.cond == true_term:
|
| H A D | search.py | 17 foldr1, boolT, word32T, word8T, builtinTs, true_term, false_term,
267 self.premise = syntax.true_term
479 assert b in [false_term, true_term]
480 if b == true_term:
552 result = {True: true_term, False: false_term}[result]
554 result = all ([x == true_term for x in xs])
555 result = {True: true_term, False: false_term}[result]
557 result = bool ([x for x in xs if x == true_term])
558 result = {True: true_term, False: false_term}[result]
561 result = bool_ops[op](* [x == true_term fo
[all...] |
| H A D | solver.py | 177 from syntax import (Expr, fresh_name, builtinTs, true_term, false_term, namespace
2013 return true_term
2026 if b == syntax.true_term:
2096 true_vals = [x for (x, v) in vals if v == syntax.true_term]
2118 if v == syntax.true_term:
2187 solv.assert_fact (true_term, {})
2189 assert solv.check_hyp (true_term, {}, force_solv = fs) == 'unsat'
|
| H A D | stack_logic.py | 709 rolling = syntax.true_term
711 for ident in idents.get (fname, [syntax.true_term]):
718 from syntax import mk_not, mk_and, true_term namespace
720 auto_callables = dict ([((ident, f, true_term), True)
721 for ident in idents.get (fname, [true_term])
749 (true_term, e_vis))]
764 from syntax import true_term namespace
773 for ident in idents.get (fname, [true_term]):
776 for ident2 in idents.get (fname2, [true_term])
817 res = syntax.mk_word32 (bounds[(fname, syntax.true_term)])
[all...] |
| H A D | syntax.py | 726 return true_term
1099 true_term = Expr ('Op', boolT, name = 'True', vals = []) variable
|
| H A D | trace_refute.py | 330 (syntax.true_term, entry_vis)))
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | elf_correlate.py | 14 from graph_refine.syntax import true_term, false_term, mk_not namespace
|