From: Brian Norris <banorris@uci.edu>
Date: Mon, 14 May 2012 19:46:14 +0000 (-0700)
Subject: nodestack: remove unnecessary conditional
X-Git-Tag: pldi2013~440
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=cb7aad2ea56679749de498472b5ee6c1471cf8f2;p=model-checker.git

nodestack: remove unnecessary conditional

I expect that we should never have a totally-empty NodeStack. It is designed
such that there is a stub 'empty' node that represents the choices at the start
of the program, when the first userprogram thread is 'created' (note: there is
no corresponding ModelAction for this first creation).
---

diff --git a/nodestack.cc b/nodestack.cc
index 7cef4b6..379fb3b 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -124,10 +124,10 @@ void NodeStack::print()
 ModelAction * NodeStack::explore_action(ModelAction *act)
 {
 	DBG();
-	if (node_list.empty()) {
-		node_list.push_back(new Node(act));
-		iter = node_list.begin();
-	} else if (get_head()->has_been_explored(act->get_tid())) {
+
+	ASSERT(!node_list.empty());
+
+	if (get_head()->has_been_explored(act->get_tid())) {
 		/* Discard duplicate ModelAction */
 		delete act;
 		iter++;