projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dfb6b17) | patch
model: print bug reports at end of each execution
authorBrian Norris <banorris@uci.edu>
Thu, 15 Nov 2012 21:33:13 +0000 (13:33 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 01:38:55 +0000 (17:38 -0800)
commit2d500fe42404f9a451051bd7fefef6b3e50db0a7
tree58bf18a61f2eca569b6707e426cdb7803ac924c8tree | snapshot
parentdfb6b1724a592f7a5376336d653b93d9010833c4commit | diff
model: print bug reports at end of each execution

This ensures:
- that bug reports are printed only at the end of feasible executions
- that execution summaries are printed only for complete (or halted and
  buggy) executions that are feasible
- that all bug reports will have the same formatting (at least, ones
  that use the 'assert_bug()' function)

Note that deadlocks are the only bugs reported this way right now. I'll
fix that up soon.
model.cc diff | blob | history
C++11 memory model checker