From 029af23cb3196ffdd986497d2c45a938af526362 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 15 Nov 2012 17:51:43 -0800 Subject: [PATCH] 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. --- model.cc | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) 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"); -- 2.34.1