Searched refs:boolT (Results 1 - 8 of 8) sorted by path
| /seL4-l4v-master/graph-refine/ |
| H A D | check.py | 21 from syntax import (true_term, false_term, boolT, mk_var, mk_word32, mk_word8, namespace
|
| H A D | debug.py | 366 if v.typ == syntax.boolT:
856 assert expr.typ == syntax.boolT, expr
|
| H A D | logic.py | 8 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node namespace
28 return Expr ('Op', boolT, name = 'ROData', vals = [m])
31 if a.typ != c.typ and c.typ == boolT:
39 if vs[i].typ.kind != 'Word' and vs[i].typ != boolT:
334 elif typ == boolT:
1544 return syntax.Expr ('Op', boolT, name = 'StackEquals',
1596 return syntax.Expr ('Op', boolT,
1599 return syntax.Expr ('Op', boolT,
1603 return syntax.Expr ('Op', boolT,
1607 elif expr.name == 'Equals' and expr.vals[0].typ == boolT
[all...] |
| H A D | rep_graph.py | 8 from syntax import (true_term, false_term, boolT, mk_and, mk_not, mk_implies, namespace
445 pc = mk_smt_expr (av ('pc_of', boolT), boolT)
553 pc = mk_smt_expr (name, boolT)
683 cond = self.p.fresh_var (name, boolT)
684 env[(cond.name, boolT)] = self.add_local_def (n,
691 success = self.solv.add_var (nm, boolT)
692 success = mk_smt_expr (success, boolT)
|
| H A D | search.py | 15 foldr1, boolT, word32T, word8T, builtinTs, true_term, false_term,
558 assert all ([x.typ == boolT for x in xs])
|
| H A D | solver.py | 176 foldr1, mk_or, boolT, word32T, word8T, mk_implies, Type, get_global_wrapper)
388 solv.note_model_expr (sexp, boolT)
1438 elif typ == syntax.boolT:
1698 var = self.add_var ('pvalid', boolT)
1705 mk_smt_expr (var, boolT))
1791 self.note_model_expr ('(= %s %s)' % (st_top, rhs), boolT)
1964 assert hyp.typ == boolT
1968 v = solv.test_hyp (mk_smt_expr (s, boolT), {})
1973 assert hyp.typ == boolT
|
| H A D | stack_logic.py | 92 syntax.boolT)
|
| H A D | syntax.py | 880 boolT = builtinTs['Bool'] variable
1097 true_term = Expr ('Op', boolT, name = 'True', vals = [])
1098 false_term = Expr ('Op', boolT, name = 'False', vals = [])
1099 unspecified_precond_term = Expr ('Op', boolT, name = 'UnspecifiedPrecond', vals = [])
1297 assert get_expr_typ(node.cond) == boolT
1351 return Expr ('Op', boolT, name = 'Equals', vals = [x, y])
1356 return Expr ('Op', boolT, name = name, vals = [x, y])
1361 return Expr ('Op', boolT, name = name, vals = [x, y])
1364 assert x.typ == boolT
1365 assert y.typ == boolT
[all...] |
Completed in 85 milliseconds