From: Brian Norris <banorris@uci.edu>
Date: Tue, 2 Oct 2012 00:20:34 +0000 (-0700)
Subject: model: always re-calculate clock vectors
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=99ca0039c04d8c3dc000f7d3899d1d81564bc168;ds=sidebyside

model: always re-calculate clock vectors

Clock vectors are mutable, via synchronization. We will need to both
snapshot and recompute clock vectors as they are generated. Right now,
we have some incorrect assumptions in place. This bugfix prevents stale
clock vectors (from previous executions) from polluting subsequent
executions.
---

diff --git a/model.cc b/model.cc
index 468900ae..c4bc693e 100644
--- a/model.cc
+++ b/model.cc
@@ -543,10 +543,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		/* Discard duplicate ModelAction; use action from NodeStack */
 		delete curr;
 
-		/* If we have diverged, we need to reset the clock vector. */
-		if (diverge == NULL) {
-			newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-		}
+		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 	} else {
 		newcurr = curr;
 		/*