From: bdemsky <bdemsky@uci.edu>
Date: Tue, 26 Nov 2019 06:06:03 +0000 (-0800)
Subject: assert_bug function fixes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f6bfb389fc2a280a4030220fd656b03c93e08ee4;p=c11tester.git

assert_bug function fixes
---

diff --git a/execution.cc b/execution.cc
index f601145a..6057ec51 100644
--- a/execution.cc
+++ b/execution.cc
@@ -183,11 +183,10 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 	}
 }
 
-bool ModelExecution::assert_bug(const char *msg)
+void ModelExecution::assert_bug(const char *msg)
 {
 	priv->bugs.push_back(new bug_message(msg));
-
-	return false;
+	set_assert();
 }
 
 /** @return True, if any bugs have been reported for this execution */
diff --git a/execution.h b/execution.h
index 5e1b1870..1a381807 100644
--- a/execution.h
+++ b/execution.h
@@ -66,7 +66,7 @@ public:
 
 	bool check_action_enabled(ModelAction *curr);
 
-	bool assert_bug(const char *msg);
+	void assert_bug(const char *msg);
 
 	bool have_bug_reports() const;
 
diff --git a/model.cc b/model.cc
index adfa971a..88b3302a 100644
--- a/model.cc
+++ b/model.cc
@@ -130,7 +130,7 @@ Thread * ModelChecker::get_next_thread()
  * @param msg Descriptive message for the bug (do not include newline char)
  * @return True if bug is immediately-feasible
  */
-bool ModelChecker::assert_bug(const char *msg, ...)
+void ModelChecker::assert_bug(const char *msg, ...)
 {
 	char str[800];
 
@@ -139,7 +139,7 @@ bool ModelChecker::assert_bug(const char *msg, ...)
 	vsnprintf(str, sizeof(str), msg, ap);
 	va_end(ap);
 
-	return execution->assert_bug(str);
+	execution->assert_bug(str);
 }
 
 /**
@@ -150,8 +150,8 @@ bool ModelChecker::assert_bug(const char *msg, ...)
 void ModelChecker::assert_user_bug(const char *msg)
 {
 	/* If feasible bug, bail out now */
-	if (assert_bug(msg))
-		switch_to_master(NULL);
+	assert_bug(msg);
+	switch_to_master(NULL);
 }
 
 /** @brief Print bug report listing for this execution (if any bugs exist) */
diff --git a/model.h b/model.h
index b974419f..3e065186 100644
--- a/model.h
+++ b/model.h
@@ -56,7 +56,7 @@ public:
 	void switch_from_master(Thread *thread);
 	uint64_t switch_to_master(ModelAction *act);
 
-	bool assert_bug(const char *msg, ...);
+	void assert_bug(const char *msg, ...);
 
 	void assert_user_bug(const char *msg);