Do not unset FuncInst locations when new executions start; check if execution numbers...

diff --git a/funcinst.cc b/funcinst.cc
index 7f031d17d9060251992e7fd13c423e1abe6a9460..c89284a70fdeccbe996df43d6cd50b53e6d0a29a 100644 (file)
--- a/funcinst.cc
+++ b/funcinst.cc
@@ -1,7 +1,9 @@
 #include "funcinst.h"
+#include "model.h"
 
 FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
-       single_location(true)
+       single_location(true),
+       execution_number(model->get_execution_number())
 {
        ASSERT(act);
        ASSERT(func_node);

diff --git a/funcinst.h b/funcinst.h
index 6bbed2c88ca452c8af13ec31e72eb156f5c50e60..ae3aa09325148a58925819c977faa4d66aa3684c 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -17,7 +17,6 @@ public:
 
        void * get_location() const { return location; }
        void set_location(void * loc) { location = loc; }
-       void unset_location() { location = NULL; }
 
        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }
@@ -37,6 +36,9 @@ public:
        bool is_single_location() { return single_location; }
        void not_single_location() { single_location = false; }
 
+       void set_execution_number(int new_number) { execution_number = new_number; }
+       int get_execution_number() { return execution_number; }
+
        void print();
 
        MEMALLOC
@@ -57,6 +59,7 @@ private:
        FuncNode * func_node;
 
        bool single_location;
+       int execution_number;
 
        /* Currently not in use. May remove this field later
         *

diff --git a/funcnode.cc b/funcnode.cc
index e05e84f7367c418eb33296fcf459d35a74149382..a402ecb42a26d399a4f5d83b9a52411055041ab1 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -5,6 +5,8 @@
 #include "predicate.h"
 #include "concretepredicate.h"
 
+#include "model.h"
+
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
        exit_count(0),
@@ -31,11 +33,6 @@ FuncNode::FuncNode(ModelHistory * history) :
 /* Reallocate snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
-       for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
-               FuncInst * inst = it->getVal();
-               inst->unset_location();
-       }
-
        action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
@@ -66,10 +63,13 @@ void FuncNode::add_inst(ModelAction *act)
                FuncInst * inst = func_inst_map.get(position);
 
                ASSERT(inst->get_type() == act->get_type());
+               int curr_execution_number = model->get_execution_number();
 
-               // locations are set to NULL when new executions start
-               if (inst->get_location() == NULL)
+               /* Reset locations when new executions start */
+               if (inst->get_execution_number() != curr_execution_number) {
                        inst->set_location(act->get_location());
+                       inst->set_execution_number(curr_execution_number);
+               }
 
                if (inst->get_location() != act->get_location())
                        inst->not_single_location();