model: add PendingFutureValue constructor
authorBrian Norris <banorris@uci.edu>
Tue, 8 Jan 2013 01:38:25 +0000 (17:38 -0800)
committerBrian Norris <banorris@uci.edu>
Tue, 8 Jan 2013 02:00:12 +0000 (18:00 -0800)
model.cc
model.h

index 98df8f3..bc17a88 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -871,7 +871,7 @@ bool ModelChecker::process_write(ModelAction *curr)
                                        pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
                                set_latest_backtrack(pfv.act);
                }
-               futurevalues->resize(0);
+               futurevalues->clear();
        }
 
        mo_graph->commitChanges();
@@ -1773,8 +1773,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                if (thin_air_constraint_may_allow(curr, act)) {
                                        if (!is_infeasible() ||
                                                        (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
-                                               struct PendingFutureValue pfv = {curr, act};
-                                               futurevalues->push_back(pfv);
+                                               futurevalues->push_back(PendingFutureValue(curr, act));
                                        }
                                }
                        }
diff --git a/model.h b/model.h
index c97cbf1..414cf93 100644 (file)
--- a/model.h
+++ b/model.h
@@ -67,7 +67,8 @@ struct execution_stats {
 };
 
 struct PendingFutureValue {
-       ModelAction *writer;
+       PendingFutureValue(ModelAction *writer, ModelAction *act) : writer(writer), act(act) { }
+       const ModelAction *writer;
        ModelAction *act;
 };