From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 01:51:43 +0000 (-0800)
Subject: model: temporary fix for uninitialized loads
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=029af23cb3196ffdd986497d2c45a938af526362

model: temporary fix for uninitialized loads

This patch does two things:

(1) Convert 'set_assert()' to 'assert_bug()' to provide:
    - More unified bug printing
    - Only printing the bug for a feasible prefix
(2) Avoids the work_queue loop if a bug was asserted

Part (1) mostly provides some cosmetic fixes.
Part (2) prevents an ASSERT() from being thrown in future values, since
we don't abort the trace early enough when there's nothing to read from.

This all needs better treatment of uninitialized loads, as there are
some loose ends.
---

diff --git a/model.cc b/model.cc
index 417252c3..3b83b569 100644
--- a/model.cc
+++ b/model.cc
@@ -1037,7 +1037,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-	while (!work_queue.empty()) {
+	while (!work_queue.empty() && !has_asserted()) {
 		WorkQueueEntry work = work_queue.front();
 		work_queue.pop_front();
 
@@ -2179,11 +2179,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		}
 	}
 
-	if (!initialized) {
-		/** @todo Need a more informative way of reporting errors. */
-		printf("ERROR: may read from uninitialized atomic\n");
-		set_assert();
-	}
+	if (!initialized)
+		assert_bug("May read from uninitialized atomic");
 
 	if (DBG_ENABLED() || !initialized) {
 		printf("Reached read action:\n");