From b4dd96124e3182bd2ae7d9d2b2ff332b3ef8fc27 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 6 Jul 2012 17:54:54 -0700 Subject: [PATCH] model: detect uninitialized atomic reads --- model.cc | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index a67163f..884ed64 100644 --- a/model.cc +++ b/model.cc @@ -323,6 +323,9 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) ASSERT(curr->is_read()); + /* Track whether this object has been initialized */ + bool initialized = false; + for (i = 0; i < thrd_lists->size(); i++) { action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; @@ -341,10 +344,27 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->get_node()->add_read_from(act); /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) + if (act->happens_before(curr)) { + initialized = true; break; + } } } + + if (!initialized) { + /* TODO: need a more informative way of reporting errors */ + printf("ERROR: may read from uninitialized atomic\n"); + } + + if (DBG_ENABLED() || !initialized) { + printf("Reached read action:\n"); + curr->print(); + printf("Printing may_read_from\n"); + curr->get_node()->print_may_read_from(); + printf("End printing may_read_from\n"); + } + + ASSERT(initialized); } static void print_list(action_list_t *list) -- 2.34.1