From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 02:29:30 +0000 (-0800)
Subject: model: check for NULL parent Node
X-Git-Tag: oopsla2013~414
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=545b5f4d69e8156d7f1b9560170262303156bbf1;p=model-checker.git

model: check for NULL parent Node

I'm editing the NodeStack to eliminate the empty Node. So we should
check to ensure that the Node has a parent before using it.
---

diff --git a/model.cc b/model.cc
index 4d6e8af..843034d 100644
--- a/model.cc
+++ b/model.cc
@@ -254,6 +254,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
 		} else {
+			ASSERT(prevnode);
 			/* Make a different thread execute for next step */
 			scheduler->add_sleep(get_thread(next->get_tid()));
 			tid = prevnode->get_next_backtrack();
@@ -1295,7 +1296,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
-	if (!parnode->backtrack_empty() ||
+	if ((parnode && !parnode->backtrack_empty()) ||
 			 !currnode->misc_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||