projects / model-checker.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ed5684e) | patch
model: pull "may_read_from set" calculation out of initialization
authorBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 23:26:52 +0000 (16:26 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 23:45:55 +0000 (16:45 -0700)
commit31246eff241f4593a33501f8c33b6eadca1d7664
tree6f7e91499098c543ae5922ce1cfe74efefbf40fetree | snapshot
parented5684e598c27e458bde4976848d48a0cd247dbbcommit | diff
model: pull "may_read_from set" calculation out of initialization

The build_reads_from_past calculation shouldn't be part of the action
initialization. It requires more information from the ModelChecker.

In the future, we will assume that all check_curren_action code (after
initialization) may include the current action in the model-checker lists. So
this also fixes up the build_reads_from_past code so that it skips the current
action.
model.cc diff | blob | history
C++11 memory model checker