From dbd7e7a54fc9a2f7121d065b9ef44f990643f4eb Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Wed, 12 Apr 2023 14:25:33 +0200 Subject: [PATCH] Inline Exploration::system_error. --- src/mc/explo/CommunicationDeterminismChecker.cpp | 4 ++-- src/mc/explo/Exploration.cpp | 9 ++------- src/mc/explo/Exploration.hpp | 3 --- 3 files changed, 4 insertions(+), 12 deletions(-) diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index 5e57a9b4f4..c36dfffe4a 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -209,7 +209,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC XBT_INFO("*********************************************************"); XBT_INFO("%s", send_diff.c_str()); exploration_.log_state(); - exploration_.system_exit(ExitStatus::NON_DETERMINISM); + throw McError(ExitStatus::NON_DETERMINISM); } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); @@ -219,7 +219,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC if (not recv_diff.empty()) XBT_INFO("%s", recv_diff.c_str()); exploration_.log_state(); - exploration_.system_exit(ExitStatus::NON_DETERMINISM); + throw McError(ExitStatus::NON_DETERMINISM); } } } diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index c23c2ed472..7a77588d61 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -113,7 +113,7 @@ XBT_ATTRIB_NORETURN void Exploration::report_crash(int status) XBT_INFO("Stack trace not shown because there is no memory introspection."); } - system_exit(ExitStatus::PROGRAM_CRASH); + throw McError(ExitStatus::PROGRAM_CRASH); } XBT_ATTRIB_NORETURN void Exploration::report_assertion_failure() { @@ -127,12 +127,7 @@ XBT_ATTRIB_NORETURN void Exploration::report_assertion_failure() "--cfg=model-check/replay:'%s'", get_record_trace().to_string().c_str()); log_state(); - system_exit(ExitStatus::SAFETY); -} - -void Exploration::system_exit(ExitStatus status) const -{ - throw McError(status); + throw McError(ExitStatus::SAFETY); } }; // namespace simgrid::mc diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index 179ebaf903..a164bf0a8f 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -51,9 +51,6 @@ public: /** Produce an error message indicating that a property was violated */ XBT_ATTRIB_NORETURN void report_assertion_failure(); - /** Kill the application and the model-checker (which exits with `status`)*/ - XBT_ATTRIB_NORETURN void system_exit(ExitStatus status) const; - /* These methods are callbacks called by the model-checking engine * to get and display information about the current state of the * model-checking algorithm: */ -- 2.20.1