From: Brian Norris <banorris@uci.edu>
Date: Wed, 10 Oct 2012 18:43:52 +0000 (-0700)
Subject: action: add NULL dereference assertion
X-Git-Tag: pldi2013~60
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1645d16c883f765168a26892f07d003963d5b68c;p=model-checker.git

action: add NULL dereference assertion

In user programs, we might find a NULL atomic object being dereferenced,
causing strange model-checker behavior which will track memory address 0
as an atomic object. This may result in apparently-uninitialized
variables, for instance.

So, just nip these in the bud with an assertion. Perhaps these things
can transformed into some more informative type of warning in the
future, where user-visible bugs might print helpful messages.
---

diff --git a/action.cc b/action.cc
index 1a819ea..ca12856 100644
--- a/action.cc
+++ b/action.cc
@@ -36,6 +36,9 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
 	cv(NULL),
 	sleep_flag(false)
 {
+	/* References to NULL atomic variables can end up here */
+	ASSERT(loc || type == MODEL_FIXUP_RELSEQ);
+
 	Thread *t = thread ? thread : thread_current();
 	this->tid = t->get_id();
 }