X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=417252c3f92ceb3a4bb7948612ca3592f1be49de;hp=a2a0a6d4d39f5c2eaf99caa7e9b743e0acda4ffb;hb=1798c510e77f37e3d79cba6a1fdad3b13ccc9674;hpb=2d500fe42404f9a451051bd7fefef6b3e50db0a7

diff --git a/model.cc b/model.cc
index a2a0a6d4..417252c3 100644
--- a/model.cc
+++ b/model.cc
@@ -417,7 +417,7 @@ bool ModelChecker::next_execution()
 		num_feasible_executions++;
 
 		if (is_deadlocked())
-			assert_bug("Deadlock detected", false);
+			assert_bug("Deadlock detected");
 
 		print_bugs();
 		checkDataRaces();
@@ -677,10 +677,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
 	}
 		//otherwise fall into the lock case
 	case ATOMIC_LOCK: {
-		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
-			printf("Lock access before initialization\n");
-			set_assert();
-		}
+		if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+			assert_bug("Lock access before initialization");
 		state->islocked = true;
 		ModelAction *unlock = get_last_unlock(curr);
 		//synchronize with the previous unlock statement
@@ -890,7 +888,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 
 	/* See if we have realized a data race */
 	if (checkDataRaces())
-		set_assert();
+		assert_bug("Datarace");
 }
 
 /**
@@ -1821,9 +1819,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 	}
 
 	// If we resolved promises or data races, see if we have realized a data race.
-	if (checkDataRaces()) {
-		set_assert();
-	}
+	if (checkDataRaces())
+		assert_bug("Datarace");
 
 	return updated;
 }