From 1645d16c883f765168a26892f07d003963d5b68c Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Wed, 10 Oct 2012 11:43:52 -0700
Subject: [PATCH] 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.
---
 action.cc | 3 +++
 1 file changed, 3 insertions(+)

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