Reduce a bit the adherance of handle_waitpid to ModelChecker

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 75eb5a6..cec73c6 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -108,15 +108,14 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
   return true;
 }
 
-void ModelChecker::handle_waitpid()
+void ModelChecker::handle_waitpid(pid_t pid_to_wait)
 {
   XBT_DEBUG("Check for wait event");
   int status;
   pid_t pid;
   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
     if (pid == -1) {
-      if (errno == ECHILD) {
-        // No more children:
+      if (errno == ECHILD) { // No more children:
         xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state");
         break;
       } else {
@@ -125,13 +124,12 @@ void ModelChecker::handle_waitpid()
       }
     }
 
-    if (pid == this->get_remote_process_memory().pid()) {
+    if (pid == pid_to_wait) {
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
         unsigned long eventmsg;
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
-                   "Could not get exit status");
+        xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid_to_wait, 0, &eventmsg) != -1, "Could not get exit status");
         status = static_cast<int>(eventmsg);
         if (WIFSIGNALED(status))
           exploration_->report_crash(status);
@@ -143,9 +141,9 @@ void ModelChecker::handle_waitpid()
         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
         errno = 0;
 #ifdef __linux__
-        ptrace(PTRACE_CONT, get_remote_process_memory().pid(), 0, WSTOPSIG(status));
+        ptrace(PTRACE_CONT, pid_to_wait, 0, WSTOPSIG(status));
 #elif defined BSD
-        ptrace(PT_CONTINUE, get_remote_process_memory().pid(), (caddr_t)1, WSTOPSIG(status));
+        ptrace(PT_CONTINUE, pid_to_wait, (caddr_t)1, WSTOPSIG(status));
 #endif
         xbt_assert(errno == 0, "Could not PTRACE_CONT");
       }

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 551d0f0..7b91263 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -31,7 +31,7 @@ public:
   Exploration* get_exploration() const { return exploration_; }
   void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 
-  void handle_waitpid();                                 // FIXME move to RemoteApp
+  void handle_waitpid(pid_t pid_to_wait);                // FIXME move to RemoteApp
   bool handle_message(const char* buffer, ssize_t size); // FIXME move to RemoteApp
 };
 

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index bef9b3e..0b735e8 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/remote/CheckerSide.hpp"
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/sosp/RemoteProcessMemory.hpp"
 #include "xbt/system_error.hpp"
 #include <csignal>
 #include <sys/wait.h>
@@ -46,7 +47,7 @@ CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
         auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
         if (events == EV_SIGNAL) {
           if (sig == SIGCHLD)
-            mc->handle_waitpid();
+            mc->handle_waitpid(mc->get_remote_process_memory().pid());
           else
             xbt_die("Unexpected signal: %d", sig);
         } else {