model: add PendingFutureValue constructor

diff --git a/model.cc b/model.cc
index 98df8f316106a5f4cce404f4cada60ee35c5898a..bc17a882c56f38c7bab1a71064f584ca285e6171 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 c97cbf1a05f905fb79087c21b91401548b5ecf2e..414cf9337c4ba638198688a8586e4eb6681fb953 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;
 };