X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=98df8f316106a5f4cce404f4cada60ee35c5898a;hb=2d685f1dc9ae1f1ace850737196e6e40d2f9e326;hp=14b1aa38b500a146e49b2766e54509afcb029c99;hpb=f19a959f1a76e35316df4b8dce39d17640305417;p=model-checker.git

diff --git a/model.cc b/model.cc
index 14b1aa3..98df8f3 100644
--- a/model.cc
+++ b/model.cc
@@ -159,7 +159,7 @@ void ModelChecker::reset_to_initial_state()
 	/* Print all model-checker output before rollback */
 	fflush(model_out);
 
-	snapshotObject->backTrackBeforeStep(0);
+	snapshot_backtrack_before(0);
 }
 
 /** @return a thread ID for a new Thread */
@@ -217,9 +217,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 		/* Do not split atomic actions. */
 		if (curr->is_rmwr())
 			return thread_current();
-		/* The THREAD_CREATE action points to the created Thread */
 		else if (curr->get_type() == THREAD_CREATE)
-			return (Thread *)curr->get_location();
+			return curr->get_thread_operand();
 	}
 
 	/* Have we completed exploring the preselected path? */
@@ -949,12 +948,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 
 	switch (curr->get_type()) {
 	case THREAD_CREATE: {
-		Thread *th = (Thread *)curr->get_location();
+		Thread *th = curr->get_thread_operand();
 		th->set_creation(curr);
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *blocking = (Thread *)curr->get_location();
+		Thread *blocking = curr->get_thread_operand();
 		ModelAction *act = get_last_action(blocking->get_id());
 		curr->synchronize_with(act);
 		updated = true; /* trigger rel-seq checks */