projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a11a861) | patch
model: rewrite mo_check_promises
authorBrian Norris <banorris@uci.edu>
Sat, 9 Feb 2013 01:08:47 +0000 (17:08 -0800)
committerBrian Norris <banorris@uci.edu>
Tue, 12 Feb 2013 19:02:33 +0000 (11:02 -0800)
commit76e48f210747b7ef23387ffd7c33ea0009c1d922
tree6991c57199c2fb6ea4cdde17d30a04d37e9c1c31tree | snapshot
parenta11a861e697310b5fd8abe52dff49fc8a66eeb78commit | diff
model: rewrite mo_check_promises

Rather than use some special logic that was devised when we didn't
include promises in the mo-graph, we can simplify our mo_check_promises
code by querying the mo-graph for reachability. This *should* be at
least as good of a 'check' as the previous code, and much less cryptic.
model.cc diff | blob | history
C++11 memory model checker