Add RMW support to core.

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 3262f5e55caf992397d9134f24f2bba325cc4e87..9fc15cd894fc48062c74ac131884fbebc530a5e2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -332,10 +332,9 @@ bool ModelChecker::isfeasible() {
 /** Process a RMW by converting previous read into a RMW. */
 void ModelChecker::process_rmw(ModelAction * act) {
        int tid = id_to_int(act->get_tid());
-       std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-       ASSERT(tid < (int) vec->size());
-       ModelAction *lastread=(*vec)[tid].back();
+       ModelAction *lastread=get_last_action(tid);
        lastread->upgrade_rmw(act);
+       cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
 }
 
 /**