Searched refs:visits (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | conflict.py | 261 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 D | trace_refute.py | 565 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 D | rep_graph.py | 20 """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 D | loop_bounds.py | 316 for (n_vc, tag) in hyp.visits ():
|
H A D | check.py | 504 # 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 D | search.py | 1530 hs = [h for h in hyps if point in [n for ((n, _), _) in h.visits ()]
|
/seL4-l4v-master/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. *)
|
Completed in 61 milliseconds