From 67cae4edb16c1c432b26bedcc9e19dae6dc37b1b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 6 Dec 2012 22:53:07 -0800 Subject: [PATCH] model/action: bugfix - UNINIT actions do not have a Node Fix the one place where ModelChecker looks for a Node in an UNINIT action. This also adds an ASSERT() within ModelAction to prevent calling get_node() on an UNINIT action. It is technically OK to call get_node() in this case, but most callers don't check for NULL, so it's better to just catch the ASSERT() for this unwanted special case. --- action.cc | 2 ++ model.cc | 5 ++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/action.cc b/action.cc index 121f5ee..d418bdb 100644 --- a/action.cc +++ b/action.cc @@ -349,6 +349,8 @@ void ModelAction::set_try_lock(bool obtainedlock) { /** @return The Node associated with this ModelAction */ Node * ModelAction::get_node() const { + /* UNINIT actions do not have a Node */ + ASSERT(!is_uninitialized()); return node; } diff --git a/model.cc b/model.cc index 1499d12..7bff598 100644 --- a/model.cc +++ b/model.cc @@ -2510,7 +2510,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) } bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { - while(true) { + while (true) { + /* UNINIT actions don't have a Node, and they never sleep */ + if (write->is_uninitialized()) + return true; Node *prevnode=write->get_node()->get_parent(); bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; -- 2.34.1