From: Brian Norris <banorris@uci.edu>
Date: Fri, 4 May 2012 06:51:26 +0000 (-0700)
Subject: model: change DEBUG() statement to ASSERT()
X-Git-Tag: pldi2013~455
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67f8065b5df1b68b7b46af2c37cc0ba601fe5345;p=model-checker.git

model: change DEBUG() statement to ASSERT()

Now that I've fixed the model-checking bug that produced this error, turn this
error message into a fail-stop ASSERT() statement. This way, I won't ignore a
bug like this in the future!
---

diff --git a/model.cc b/model.cc
index e323825..7678968 100644
--- a/model.cc
+++ b/model.cc
@@ -86,8 +86,9 @@ Thread * ModelChecker::schedule_next_thread()
 	if (nextThread == THREAD_ID_T_NONE)
 		return NULL;
 	t = thread_map[id_to_int(nextThread)];
-	if (t == NULL)
-		DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+
+	ASSERT(t != NULL);
+
 	return t;
 }