Searched refs:visits (Results 1 - 8 of 8) sorted by path
| /seL4-l4v-10.1.1/HOL4/src/search/ |
| H A D | bftScript.sml | 157 (* If BFT visits x, then x is reachable or is in the starting accumulator *)
180 (* in seen, then BFT visits x. *)
|
| H A D | dftScript.sml | 162 (* If DFT visits x, then x is reachable or is in the starting accumulator *)
181 (* in seen, then DFT visits x. *)
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | check.py | 506 # if we can reach node n with (y - 1) visits to n, then the next
507 # node will have y visits to n, which we are disallowing
527 # the matching rhs visits when checking lhs consts
735 for n_vc in hyp2.visits ()])
795 return 'visits to %d' % split
800 return 'visits [%d, %d, %d ...] to %d' % (i, j, k, split)
810 v = syntax.mk_var ('#seq-visits', word32T)
824 printout (' Prove the number of visits to %d is in %s'
|
| H A D | loop_bounds.py | 310 for (n_vc, tag) in hyp.visits ():
|
| H A D | rep_graph.py | 22 """Used to represent a target number of visits to a split point.
183 def visits (self): member in class:Hyp
303 by visits 0, 1, 2, 3, i, and i + 1 (for a symbolic value i). The
304 variable state at visits 4 and i + 2 will be calculated but no
356 for (split, visits) in vcount:
358 and visits.kind == 'Options'):
|
| H A D | search.py | 1532 hs = [h for h in hyps if point in [n for ((n, _), _) in h.visits ()]
|
| H A D | trace_refute.py | 567 for (stack, visits, verdict) in vs:
569 for (addr, i) in visits]))
581 [stack, visits, verdict] = bits
583 visits = parse_num_arrow_list (visits)
587 fn = identify_function (stack, visits)
589 verdicts[fn].append ((stack, visits, verdict))
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | conflict.py | 264 def emitInconsistentTrace(fout, full_context,visits,line=None):
270 for x in visits:
280 max_stack_i =max(visits, key = lambda x: x[1])[1]
315 #one_context is true iff all visits lie in context 0
316 def emitInconsistent(fout, context,visits):
317 if visits == []:
325 if all ([l > 0 for (_, l) in visits]):
326 m = min ([l for (_, l) in visits])
327 visits = [(baddr, l - m) for (baddr, l) in visits]
[all...] |
Completed in 130 milliseconds