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 417252c3f92ceb3a4bb7948612ca3592f1be49de..3b83b569baf5c12f356aaf596023ca4fe3b3cde2 100644 (file)
--- 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");