From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Dec 2012 06:53:07 +0000 (-0800)
Subject: model/action: bugfix - UNINIT actions do not have a Node
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67cae4edb16c1c432b26bedcc9e19dae6dc37b1b;p=cdsspec-compiler.git

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

Fix the one place where ModelChecker looks for a Node in an UNINIT
action.

This also adds an ASSERT() within ModelAction to prevent calling
get_node() on an UNINIT action. It is technically OK to call get_node()
in this case, but most callers don't check for NULL, so it's better to
just catch the ASSERT() for this unwanted special case.
---

diff --git a/action.cc b/action.cc
index 121f5ee..d418bdb 100644
--- a/action.cc
+++ b/action.cc
@@ -349,6 +349,8 @@ void ModelAction::set_try_lock(bool obtainedlock) {
 /** @return The Node associated with this ModelAction */
 Node * ModelAction::get_node() const
 {
+	/* UNINIT actions do not have a Node */
+	ASSERT(!is_uninitialized());
 	return node;
 }
 
diff --git a/model.cc b/model.cc
index 1499d12..7bff598 100644
--- a/model.cc
+++ b/model.cc
@@ -2510,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;