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/?p=model-checker.git;a=commitdiff_plain;h=1645d16c883f765168a26892f07d003963d5b68c

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();
 }