Inline a function in ModelChecker

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 5aa7399..c95d4bf 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -105,13 +105,6 @@ void ModelChecker::setup_ignore()
   process.ignore_global_variable("counter");
 }
 
-void ModelChecker::resume()
-{
-  if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
-    throw xbt::errno_error();
-  remote_process_memory_->clear_cache();
-}
-
 static void MC_report_crash(Exploration* explorer, int status)
 {
   XBT_INFO("**************************");
@@ -287,7 +280,11 @@ void ModelChecker::handle_waitpid()
 
 void ModelChecker::wait_for_requests()
 {
-  this->resume();
+  /* Resume the application */
+  if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
+    throw xbt::errno_error();
+  remote_process_memory_->clear_cache();
+
   if (this->get_remote_process_memory().running())
     checker_side_.dispatch();
 }

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 16fdee4..5fc0052 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -31,7 +31,6 @@ public:
   Channel& channel() { return checker_side_.get_channel(); }
 
   void start();
-  void resume();
   void wait_for_requests();
 
   /** Let the application take a transition. A new Transition is created iff the last parameter is true */