| /seL4-l4v-master/graph-refine/ |
| H A D | c_rodata.py | 32 syntax.mk_not (eq_rodata)), (n, vc))
|
| H A D | stack_logic.py | 93 (mk_nimp, mk_not) = (syntax.mk_n_implies, syntax.mk_not)
97 elif rep.test_hyp_whyps (mk_nimp (bool_hyps, mk_not (cond_exp)),
105 bool_hyps = bool_hyps + [syntax.mk_not (cond_exp)])
711 rolling = syntax.mk_and (rolling, syntax.mk_not (ident))
716 from syntax import mk_not, mk_and, true_term namespace
754 if rep.test_hyp_whyps (mk_not (mk_and (pc, cond2)),
944 from syntax import mk_not, mk_and, foldr1 namespace
958 new = foldr1 (mk_and, [pc] + [syntax.mk_not (
961 if rep.test_hyp_whyps (mk_not (ne
[all...] |
| H A D | loop_bounds.py | 12 from syntax import mk_not, true_term, false_term, mk_implies, Expr, Type, unspecified_precond_term,mk_and namespace
171 hyp = mk_implies (mk_not (epc), mk_not (pc))
527 return rep.test_hyp_whyps (syntax.mk_not (continue_to_split_guess),
|
| H A D | logic.py | 13 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
609 return foldr1 (mk_and, align_req + size_req + [mk_not (mk_eq (p, w0)),
686 return syntax.mk_not (v)
1593 return syntax.mk_not (x)
1614 return strengthen_hyp (syntax.mk_not (vals[1]), sign)
1640 return mk_and (x, mk_not (y))
1643 return norm_neg (mk_not (expr))
|
| H A D | search.py | 14 from syntax import (mk_and, mk_cast, mk_implies, mk_not, mk_uminus, mk_var, namespace
94 hyp = mk_implies (mk_not (epc), mk_not (pc))
178 if rep.test_hyp_whyps (mk_not (pc), hyps + err_pc_hyps):
1036 nrerr_pc = mk_not (rep.get_pc (('Err', err_restrs), tag = r_tag))
1568 for assn in logic.split_conjuncts (mk_not (err_cond))
1654 if rep.test_hyp_whyps (mk_not (loop_cond), hyps):
1659 hyp = mk_not (mk_and (loop_cond, ret_cond))
1793 elif rep.test_hyp_whyps (mk_not (pc), hyps):
|
| H A D | rep_graph.py | 8 from syntax import (true_term, false_term, boolT, mk_and, mk_not, mk_implies, namespace
687 rpc = mk_and (mk_not (cond), pc)
969 if self.solv.test_hyp (mk_not (pc), env):
|
| H A D | syntax.py | 719 return mk_not (self.cond)
1384 def mk_not (x): function
1488 mk_eq, mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32,
|
| H A D | pseudo_compile.py | 15 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
|
| H A D | solver.py | 1289 goal = smt_expr (syntax.mk_not (hyp), env, self)
2168 r = solv.test_hyp (syntax.mk_not (fun.nodes[n].cond), env)
|
| H A D | check.py | 22 mk_plus, mk_minus, word32T, word8T, mk_and, mk_eq, mk_implies, mk_not,
|
| /seL4-l4v-master/graph-refine/graph-to-graph/ |
| H A D | elf_correlate.py | 11 from graph_refine.syntax import true_term, false_term, mk_not namespace
|