| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | trace_refute.py | 14 import rep_graph namespace
155 err_vis_opts = rep_graph.vc_options ([0, 1, 2], [1])
159 free_hyps.append (rep_graph.pc_false_hyp (err_vis))
178 restrs = tuple ([(l_id, rep_graph.vc_offs (0))])
180 restrs = tuple ([(l_id, rep_graph.vc_offs (1))])
197 return rep_graph.pc_true_hyp (get_vis (rep.p, n,
255 hyps = rep_graph.mk_function_link_hyps (p, vis, to_tags['ASM'],
262 hyps += rep_graph.mk_function_link_hyps (p, vis, to_tags['C'])
324 from rep_graph import eq_hyp
482 rep = rep_graph
[all...] |
| H A D | stats.py | 4 from rep_graph import vc_options
11 import rep_graph namespace
118 rep = rep_graph.mk_graph_slice (p, fast = True)
|
| H A D | stack_logic.py | 12 import rep_graph namespace
28 general = [(n2, rep_graph.vc_options ([0], [1]))
31 specific = [(head, rep_graph.vc_offs (1)) for _ in [1] if head]
170 hyp = rep_graph.pc_false_hyp ((default_n_vc (p, n), tag))
181 rep = rep_graph.mk_graph_slice (p, fast = True)
201 hyp = rep_graph.pc_true_hyp ((n_vc, p.node_tags[n][0]))
647 rep = rep_graph.mk_graph_slice (p, fast = True)
737 rep = rep_graph.mk_graph_slice (p, fast = True)
738 err_hyp = rep_graph.pc_false_hyp ((default_n_vc (p, 'Err'), 'Target'))
748 hyps = [err_hyp, rep_graph
[all...] |
| H A D | search.py | 13 from rep_graph import (mk_graph_slice, vc_num, vc_offs, vc_upto,
15 import rep_graph namespace
140 rep = rep_graph.mk_graph_slice (p)
146 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
172 rep = rep_graph.mk_graph_slice (p)
174 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
755 rep = rep_graph.mk_graph_slice (p)
776 rep = rep_graph.mk_graph_slice (p, fast = True)
804 eqs = [rep_graph.eq_hyp ((expr,
808 vis_hyp = rep_graph
[all...] |
| H A D | loop_bounds.py | 1 import check,search,problem,syntax,solver,logic,rep_graph,re namespace
2 from rep_graph import vc_num, vc_offs, pc_true_hyp, Hyp, eq_hyp
7 from rep_graph import mk_graph_slice, VisitCount, to_smt_expr
96 restrs = tuple( [(n2, rep_graph.vc_options([0],[1])) for n2 in others] )
116 general = [(n2, rep_graph.vc_options ([0], [1]))
121 return [(n, tuple (general + [(head, rep_graph.vc_num (1))])),
122 (n, tuple (general + [(head, rep_graph.vc_offs (1))]))]
123 specific = [(head, rep_graph.vc_offs (1)) for _ in [1] if head]
136 ret += [rep_graph.pc_false_hyp((n_vc, p.node_tags[x][0]))
193 rep = rep_graph
[all...] |
| H A D | inst_logic.py | 12 import rep_graph namespace
|
| H A D | graph-refine.py | 15 import rep_graph namespace
|
| H A D | debug.py | 17 import rep_graph namespace
688 rep = rep_graph.mk_graph_slice (p)
705 rep = rep_graph.mk_graph_slice (p)
850 hyp = rep_graph.pc_true_hyp (((n, restrs), tag))
859 return rep_graph.eq_hyp ((expr, vis), (syntax.true_term, vis))
|
| H A D | check.py | 11 from rep_graph import mk_graph_slice, Hyp, eq_hyp, pc_true_hyp, pc_false_hyp
12 import rep_graph namespace
19 from rep_graph import (vc_num, vc_offs, vc_double_range, vc_upto, mk_vc_opts,
110 except rep_graph.InlineEvent:
481 return rep_graph.pc_triv_hyp (((n, (restr, ) + restrs),
528 rpc_triv_hyp = rep_graph.pc_triv_hyp (r_visit)
546 rep_graph.pc_triv_hyp (r_cont)] + hyps
595 return rep_graph.true_if_at_hyp (pred, vis)
645 goal = rep_graph.true_if_at_hyp (pred, cont)
657 true_next = rep_graph
[all...] |