projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 619d877) | patch
model: print bug reports only for feasible executions
authorBrian Norris <banorris@uci.edu>
Thu, 13 Dec 2012 08:36:04 +0000 (00:36 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 13 Dec 2012 08:36:04 +0000 (00:36 -0800)
commit6f45039487a95c7fb8023a2aa08b9d9085f6985e
treed350de1b49b565d69d6359b7930c99c21fcb1f3btree | snapshot
parent619d877631496c14df5e2118933e44baab6fdf4ccommit | diff
model: print bug reports only for feasible executions

We can assert a bug (e.g., uninitialized load) without having a feasible
exeuction. If this execution is later ruled infeasible, we don't need to
print the trace info.
model.cc diff | blob | history
C++11 memory model checker