model/action: bugfix - UNINIT actions do not have a Node

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a5b06ddc3358e0b82f2f353333cad576981379a2..7bff598f974e762daecc27d7d58926bdfa466d68 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2462,16 +2462,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ModelAction *last_sc_write = NULL;
 
-       /* Track whether this object has been initialized */
-       bool initialized = false;
-
-       if (curr->is_seqcst()) {
+       if (curr->is_seqcst())
                last_sc_write = get_last_seq_cst_write(curr);
-               /* We have to at least see the last sequentially consistent write,
-                        so we are initialized. */
-               if (last_sc_write != NULL)
-                       initialized = true;
-       }
 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
@@ -2503,17 +2495,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr)) {
-                               initialized = true;
+                       if (act->happens_before(curr))
                                break;
-                       }
                }
        }
 
-       if (!initialized)
-               assert_bug("May read from uninitialized atomic");
-
-       if (DBG_ENABLED() || !initialized) {
+       if (DBG_ENABLED()) {
                model_print("Reached read action:\n");
                curr->print();
                model_print("Printing may_read_from\n");
@@ -2523,7 +2510,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
-       while(true) {
+       while (true) {
+               /* UNINIT actions don't have a Node, and they never sleep */
+               if (write->is_uninitialized())
+                       return true;
                Node *prevnode=write->get_node()->get_parent();
 
                bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;