| /seL4-l4v-master/graph-refine/ |
| H A D | loop_bounds.py | 7 import check,search,problem,syntax,solver,logic,rep_graph,re namespace
8 from rep_graph import vc_num, vc_offs, pc_true_hyp, Hyp, eq_hyp
13 from rep_graph import mk_graph_slice, VisitCount, to_smt_expr
102 restrs = tuple( [(n2, rep_graph.vc_options([0],[1])) for n2 in others] )
122 general = [(n2, rep_graph.vc_options ([0], [1]))
127 return [(n, tuple (general + [(head, rep_graph.vc_num (1))])),
128 (n, tuple (general + [(head, rep_graph.vc_offs (1))]))]
129 specific = [(head, rep_graph.vc_offs (1)) for _ in [1] if head]
142 ret += [rep_graph.pc_false_hyp((n_vc, p.node_tags[x][0]))
199 rep = rep_graph
[all...] |
| H A D | trace_refute.py | 12 import rep_graph namespace
153 err_vis_opts = rep_graph.vc_options ([0, 1, 2], [1])
157 free_hyps.append (rep_graph.pc_false_hyp (err_vis))
176 restrs = tuple ([(l_id, rep_graph.vc_offs (0))])
178 restrs = tuple ([(l_id, rep_graph.vc_offs (1))])
195 return rep_graph.pc_true_hyp (get_vis (rep.p, n,
253 hyps = rep_graph.mk_function_link_hyps (p, vis, to_tags['ASM'],
260 hyps += rep_graph.mk_function_link_hyps (p, vis, to_tags['C'])
322 from rep_graph import eq_hyp
480 rep = rep_graph
[all...] |
| H A D | stats.py | 10 from rep_graph import vc_options
17 import rep_graph namespace
124 rep = rep_graph.mk_graph_slice (p, fast = True)
|
| H A D | check.py | 9 from rep_graph import mk_graph_slice, Hyp, eq_hyp, pc_true_hyp, pc_false_hyp
10 import rep_graph namespace
17 from rep_graph import (vc_num, vc_offs, vc_double_range, vc_upto, mk_vc_opts,
108 except rep_graph.InlineEvent:
479 return rep_graph.pc_triv_hyp (((n, (restr, ) + restrs),
526 rpc_triv_hyp = rep_graph.pc_triv_hyp (r_visit)
544 rep_graph.pc_triv_hyp (r_cont)] + hyps
593 return rep_graph.true_if_at_hyp (pred, vis)
643 goal = rep_graph.true_if_at_hyp (pred, cont)
655 true_next = rep_graph
[all...] |
| H A D | search.py | 11 from rep_graph import (mk_graph_slice, vc_num, vc_offs, vc_upto,
13 import rep_graph namespace
138 rep = rep_graph.mk_graph_slice (p)
144 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
170 rep = rep_graph.mk_graph_slice (p)
172 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
753 rep = rep_graph.mk_graph_slice (p)
774 rep = rep_graph.mk_graph_slice (p, fast = True)
802 eqs = [rep_graph.eq_hyp ((expr,
806 vis_hyp = rep_graph
[all...] |
| H A D | stack_logic.py | 10 import rep_graph namespace
26 general = [(n2, rep_graph.vc_options ([0], [1]))
29 specific = [(head, rep_graph.vc_offs (1)) for _ in [1] if head]
168 hyp = rep_graph.pc_false_hyp ((default_n_vc (p, n), tag))
179 rep = rep_graph.mk_graph_slice (p, fast = True)
199 hyp = rep_graph.pc_true_hyp ((n_vc, p.node_tags[n][0]))
645 rep = rep_graph.mk_graph_slice (p, fast = True)
735 rep = rep_graph.mk_graph_slice (p, fast = True)
736 err_hyp = rep_graph.pc_false_hyp ((default_n_vc (p, 'Err'), 'Target'))
746 hyps = [err_hyp, rep_graph
[all...] |
| H A D | inst_logic.py | 10 import rep_graph namespace
|
| H A D | debug.py | 15 import rep_graph namespace
686 rep = rep_graph.mk_graph_slice (p)
703 rep = rep_graph.mk_graph_slice (p)
848 hyp = rep_graph.pc_true_hyp (((n, restrs), tag))
857 return rep_graph.eq_hyp ((expr, vis), (syntax.true_term, vis))
|
| H A D | graph-refine.py | 13 import rep_graph namespace
|