From f6bfb389fc2a280a4030220fd656b03c93e08ee4 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 25 Nov 2019 22:06:03 -0800 Subject: [PATCH] assert_bug function fixes --- execution.cc | 5 ++--- execution.h | 2 +- model.cc | 8 ++++---- model.h | 2 +- 4 files changed, 8 insertions(+), 9 deletions(-) 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); -- 2.34.1