this is the bad line...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 2fa54d6e9ba1e76be577ec0625f6138ee7d1c5d4..f67b552dcd74ce3db332c2b157cc2515d600072f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -388,7 +388,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
                        break;
 
                /* Don't backtrack into a point where the thread is disabled or sleeping. */
-               if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+               if (node->enabled_status(tid)!=THREAD_ENABLED)
                        continue;
        
                /* Check if this has been explored already */
@@ -1094,7 +1094,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                                ModelAction *act=*rit;
                                bool foundvalue = false;
                                for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-                                       if (act->get_node()->get_read_from_at(i)==write) {
+                                       if (act->get_node()->get_read_from_at(j)==write) {
                                                foundvalue = true;
                                                break;
                                        }
@@ -2025,7 +2025,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
        while(true) {
                Node *prevnode=write->get_node()->get_parent();
-               bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+               
+               bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
                if (write->is_release()&&thread_sleep)
                        return true;
                if (!write->is_rmw()) {