bugfix: straighten out STL vector allocation (snapshotted vs. persistent)

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index b4a365595314b4e3dd9a9cc7d5633374d9bc3d3e..031f6a935ec5701bdf72fdf2bdfe321e70712a28 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -392,17 +392,16 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
 
-       Thread *th = get_thread(curr);
-
        bool updated = false;
+
        if (curr->is_read()) {
-               updated = process_read(curr, th, second_part_of_rmw);
+               updated = process_read(curr, get_thread(curr), second_part_of_rmw);
        }
 
        if (curr->is_write()) {
                bool updated_mod_order = w_modification_order(curr);
                bool updated_promises = resolve_promises(curr);
-               updated = updated_mod_order|updated_promises;
+               updated = updated || updated_mod_order || updated_promises;
 
                if (promises->size()==0) {
                        for (unsigned int i = 0; i<futurevalues->size(); i++) {
@@ -415,7 +414,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                }
 
                mo_graph->commitChanges();
-               th->set_return_value(VALUE_NONE);
+               get_thread(curr)->set_return_value(VALUE_NONE);
        }
 
        if (updated)
@@ -781,13 +780,15 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * false otherwise
  */
 bool ModelChecker::release_seq_head(const ModelAction *rf,
-                std::vector<const ModelAction *> *release_heads) const
+                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const
 {
-       ASSERT(rf->is_write());
        if (!rf) {
                /* read from future: need to settle this later */
                return false; /* incomplete */
        }
+
+       ASSERT(rf->is_write());
+
        if (rf->is_release())
                release_heads->push_back(rf);
        if (rf->is_rmw()) {
@@ -885,7 +886,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
  * @see ModelChecker::release_seq_head
  */
 void ModelChecker::get_release_seq_heads(ModelAction *act,
-                std::vector<const ModelAction *> *release_heads)
+                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads)
 {
        const ModelAction *rf = act->get_reads_from();
        bool complete;
@@ -921,7 +922,7 @@ bool ModelChecker::resolve_release_sequences(void *location)
        while (it != list->end()) {
                ModelAction *act = *it;
                const ModelAction *rf = act->get_reads_from();
-               std::vector<const ModelAction *> release_heads;
+               std::vector< const ModelAction *, MyAlloc<const ModelAction *> > release_heads;
                bool complete;
                complete = release_seq_head(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {