| /seL4-l4v-master/graph-refine/ |
| H A D | graph-refine.py | 19 from target_objects import trace, tracer, printout namespace
36 printout ('Testing Function pair %s' % pair)
39 printout (' (function pairing %d of %d)' % (i + 1, n))
43 printout ('Skipping %s, underspecified %s' % (pair, tag))
60 printout (' .. built problem, finding proof')
62 printout ('Problem has loop!')
66 printout ('No loop in problem.')
71 printout (' .. proof found.')
79 printout ('Refinement proven.')
81 printout ('Refinemen
[all...] |
| H A D | target_objects.py | 58 def printout (s): function
69 printout (s)
72 printout (s)
|
| H A D | inst_logic.py | 17 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
154 printout ('Warning: asm instruction name: formatting: %r'
190 printout ('Function %r contains unhandled instructions:' % f)
191 printout (' %s' % unhandled[f])
|
| H A D | check.py | 15 from target_objects import functions, pairings, trace, printout namespace
814 printout ('Step %d: %s' % (step_num, ctxt))
822 printout (' Prove the number of visits to %d is in %s'
829 printout (' Proving a predicate by future induction.')
832 printout (' proving these invariants by %d-induction' % n)
834 printout (' %s (@ addr %s)'
836 printout (' then establishing this predicate')
838 printout (' %s (@ addr %s)'
840 printout (' at large iterations (%d) and by back induction.'
851 printout (' prov
[all...] |
| H A D | stack_logic.py | 15 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
542 printout ("Stack analysis issue at (%d, %s)."
654 printout (' (stack analysis also involves %s)'
766 printout ('Doing stack analysis for %r. (%d of %d)' % (fname,
862 printout ('Doing recursion analysis for function group:')
863 printout (' %s' % list(group))
1195 printout ('Computed recursion limits.')
1198 printout ('Computed stack bounds.')
1247 printout ('Computing stack bounds.')
1339 printout ('Syntheti
[all...] |
| H A D | logic.py | 18 from target_objects import trace, printout namespace
880 printout ('add %s at %d' % (diff, n))
881 printout (' %s, %s, %s, %s' % (len (vs), len (cont_vs), len (lvals), len (rvals)))
1290 printout ('Warning: %s: no aligned instructions' % f)
1294 printout ('target mismatch on func %s' % f)
1295 printout (' (starts at 0x%x not 0x%x)' % (addr, addr2))
1299 printout ('entry mismatch on func %s' % f)
1300 printout (' (enters at 0x%x not 0x%x)' % (addr3, addr2))
|
| H A D | problem.py | 11 from target_objects import functions, pairings, trace, printout namespace
83 printout ('Aborting %s: underspecified %s' % (
514 printout ('Aborting %s: undefined symbols %s' % (self.name, symbs))
781 printout ('Aborting %s, complex loop' % p.name)
|
| H A D | search.py | 21 from target_objects import trace, printout namespace
59 printout (repr (proof))
1706 printout ("Discovered that points [%s] can be bounded"
1709 printout (" (in %s)" % name)
1720 printout ("Decided to case split at %s" % str (details))
1721 printout (" (in %s)" % name)
1725 printout ('Found a future induction at %s' % str (details[0]))
1731 printout ("Discovered a loop relation for split points %s"
1733 printout (" (in %s)" % name)
1736 printout ('No
[all...] |
| H A D | trace_refute.py | 18 from target_objects import functions, trace, pairings, symbols, printout namespace
126 printout ('Building compound problem for %s' % fnames)
|
| H A D | rep_graph.py | 15 from target_objects import functions, pairings, sections, trace, printout namespace
404 printout ([n for (n, vc) in prev_chain])
|
| H A D | solver.py | 177 from target_objects import structs, rodata, sections, trace, printout namespace
1492 printout ("WARNING: inconsistent sat/unsat.")
|
| /seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | make_hol_acl2_defaxioms.ml | 5 (* printout of the definitions in hol_defaxiomsTheory. *)
|