Sanitize MC finalization process and inline a function

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 80101e4..9e3f27f 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -109,7 +109,6 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
 
 void Api::s_close()
 {
-  remote_app_.reset();
   if (simgrid::mc::property_automaton != nullptr) {
     xbt_automaton_free(simgrid::mc::property_automaton);
     simgrid::mc::property_automaton = nullptr;

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 5edd18c..d4c8961 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -97,7 +97,12 @@ RemoteApp::RemoteApp(const std::function<void()>& code)
 
 RemoteApp::~RemoteApp()
 {
-  this->close();
+  initial_snapshot_ = nullptr;
+  if (model_checker_) {
+    model_checker_->shutdown();
+    model_checker_   = nullptr;
+    mc_model_checker = nullptr;
+  }
 }
 
 void RemoteApp::restore_initial_state() const
@@ -120,16 +125,6 @@ void RemoteApp::log_state() const
   }
 }
 
-void RemoteApp::close()
-{
-  initial_snapshot_ = nullptr;
-  if (model_checker_) {
-    model_checker_->shutdown();
-    model_checker_   = nullptr;
-    mc_model_checker = nullptr;
-  }
-}
-
 unsigned long RemoteApp::get_maxpid() const
 {
   return model_checker_->get_remote_process().get_maxpid();

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 377b99f..e88c168 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -43,7 +43,6 @@ public:
   explicit RemoteApp(const std::function<void()>& code);
 
   ~RemoteApp();
-  void close();
 
   void restore_initial_state() const;
 

diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index 769c14c..df44857 100644 (file)
--- a/src/mc/explo/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -81,6 +81,5 @@ int main(int argc, char** argv)
     res = SIMGRID_MC_EXIT_LIVENESS;
   }
   simgrid::mc::Api::get().s_close();
-  checker.release(); // FIXME: this line should not exist, but it segfaults in liveness
   return res;
 }