assert_bug function fixes

diff --git a/execution.cc b/execution.cc
index f601145a69ad3b96c5d487962089e406f09c07e5..6057ec51929db5f89e7646b7937e135dddcf94a5 100644 (file)
--- 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 5e1b18700c248736d7657f04c625eaea1c18b277..1a38180728ef79bac50cd434aea0a5fcab2cf52b 100644 (file)
--- 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 adfa971a3dd35c6fad556b1d0e09a49fe9338eae..88b3302acd5804a2a0756e818e5e9fc98092e0de 100644 (file)
--- 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 b974419fe851e3042088ee94a322d99201e1cd46..3e0651864d80f97d5ff01a11b758ec77871867b4 100644 (file)
--- 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);