Inline Exploration::system_error.

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index 5e57a9b..c36dfff 100644 (file)
--- 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 c23c2ed..7a77588 100644 (file)
--- 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 179ebaf..a164bf0 100644 (file)
--- 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: */