From 1501c3cf268534e96d8011dbf4ecd829526f2a7a Mon Sep 17 00:00:00 2001 From: weiyu Date: Fri, 30 Aug 2019 13:04:20 -0700 Subject: [PATCH] remove a redundant member function that I added before --- execution.cc | 10 ---------- execution.h | 1 - model.cc | 2 +- 3 files changed, 1 insertion(+), 12 deletions(-) diff --git a/execution.cc b/execution.cc index 9ee91570..524c6fa2 100644 --- a/execution.cc +++ b/execution.cc @@ -199,16 +199,6 @@ bool ModelExecution::have_bug_reports() const return priv->bugs.size() != 0; } -/** @return True, if any fatal bugs have been reported for this execution. - * Any bug other than a data race is considered a fatal bug. Data races - * are not considered fatal unless the number of races is exceeds - * a threshold (temporarily set as 15). - */ -bool ModelExecution::have_fatal_bug_reports() const -{ - return priv->bugs.size() != 0; -} - SnapVector * ModelExecution::get_bugs() const { return &priv->bugs; diff --git a/execution.h b/execution.h index a6add070..24738828 100644 --- a/execution.h +++ b/execution.h @@ -70,7 +70,6 @@ public: bool assert_bug(const char *msg); bool have_bug_reports() const; - bool have_fatal_bug_reports() const; SnapVector * get_bugs() const; diff --git a/model.cc b/model.cc index 0a2e844d..ce598cfa 100644 --- a/model.cc +++ b/model.cc @@ -363,7 +363,7 @@ bool ModelChecker::should_terminate_execution() /* Infeasible -> don't take any more steps */ if (execution->is_infeasible()) return true; - else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) { + else if (execution->isfeasibleprefix() && execution->have_bug_reports()) { execution->set_assert(); return true; } else if (execution->isFinished()) { -- 2.34.1