Searched refs:visits (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-master/graph-refine/graph-to-graph/
H A Dconflict.py261 def emitInconsistentTrace(fout, full_context,visits,line=None):
267 for x in visits:
277 max_stack_i =max(visits, key = lambda x: x[1])[1]
312 #one_context is true iff all visits lie in context 0
313 def emitInconsistent(fout, context,visits):
314 if visits == []:
322 if all ([l > 0 for (_, l) in visits]):
323 m = min ([l for (_, l) in visits])
324 visits = [(baddr, l - m) for (baddr, l) in visits]
[all...]
/seL4-l4v-master/graph-refine/
H A Dtrace_refute.py565 for (stack, visits, verdict) in vs:
567 for (addr, i) in visits]))
579 [stack, visits, verdict] = bits
581 visits = parse_num_arrow_list (visits)
585 fn = identify_function (stack, visits)
587 verdicts[fn].append ((stack, visits, verdict))
H A Drep_graph.py20 """Used to represent a target number of visits to a split point.
181 def visits (self): member in class:Hyp
301 by visits 0, 1, 2, 3, i, and i + 1 (for a symbolic value i). The
302 variable state at visits 4 and i + 2 will be calculated but no
354 for (split, visits) in vcount:
356 and visits.kind == 'Options'):
H A Dloop_bounds.py316 for (n_vc, tag) in hyp.visits ():
H A Dcheck.py504 # if we can reach node n with (y - 1) visits to n, then the next
505 # node will have y visits to n, which we are disallowing
525 # the matching rhs visits when checking lhs consts
733 for n_vc in hyp2.visits ()])
793 return 'visits to %d' % split
798 return 'visits [%d, %d, %d ...] to %d' % (i, j, k, split)
808 v = syntax.mk_var ('#seq-visits', word32T)
822 printout (' Prove the number of visits to %d is in %s'
H A Dsearch.py1530 hs = [h for h in hyps if point in [n for ((n, _), _) in h.visits ()]
/seL4-l4v-master/HOL4/src/search/
H A DbftScript.sml157 (* If BFT visits x, then x is reachable or is in the starting accumulator *)
180 (* in seen, then BFT visits x. *)
H A DdftScript.sml162 (* If DFT visits x, then x is reachable or is in the starting accumulator *)
181 (* in seen, then DFT visits x. *)

Completed in 61 milliseconds