X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4f9095b90297e111f30558615fde2567f5710e99..d2e206d0539afade3722f7aa9f7a65ad8a714253:/src/mc/ModelChecker.cpp?ds=sidebyside

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 15d5d835fc..1bbf9e6440 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -277,7 +277,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
 
   case MC_MESSAGE_ASSERTION_FAILED:
     MC_report_assertion_error();
-    ::exit(SIMGRID_MC_EXIT_SAFETY);
+    this->exit(SIMGRID_MC_EXIT_SAFETY);
     break;
 
   default:
@@ -287,6 +287,15 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   return true;
 }
 
+/** Terminate the model-checker aplication */
+void ModelChecker::exit(int status)
+{
+  // TODO, terminate the model checker politely instead of exiting rudel
+  if (process().running())
+    kill(process().pid(), SIGKILL);
+  ::exit(status);
+}
+
 bool ModelChecker::handle_events()
 {
   char buffer[MC_MESSAGE_LENGTH];
@@ -384,7 +393,7 @@ void ModelChecker::handle_waitpid()
           xbt_die("Could not get exit status");
         if (WIFSIGNALED(status)) {
           MC_report_crash(status);
-          ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+          mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
       }