X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7f5e78a43b4bed7bae8304ad12de6e2e555b34db..8b3a964a05100f371bc65e4bdad591d06cb09165:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 4250bffe34..2b1d6d980c 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -141,17 +141,19 @@ static void MC_report_crash(int status)
     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
   else if (WIFEXITED(status))
     XBT_INFO("From exit: %i", WEXITSTATUS(status));
-  if (WCOREDUMP(status))
-    XBT_INFO("A core dump was generated by the system.");
-  else
-    XBT_INFO("No core dump was generated by the system.");
+  if (not xbt_log_no_loc)
+    XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
   XBT_INFO("Counter-example execution trace:");
   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();
-  XBT_INFO("Stack trace:");
-  mc_model_checker->process().dump_stack();
+  if (xbt_log_no_loc) {
+    XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
+  } else {
+    XBT_INFO("Stack trace:");
+    mc_model_checker->process().dump_stack();
+  }
 }
 
 static void MC_report_assertion_error()
@@ -336,7 +338,10 @@ void ModelChecker::handle_waitpid()
           xbt_die("Could not PTRACE_CONT");
       }
 
-      else if (WIFEXITED(status) || WIFSIGNALED(status)) {
+      else if (WIFSIGNALED(status)) {
+        MC_report_crash(status);
+        mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+      } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
         this->process().terminate();
       }
@@ -362,8 +367,8 @@ void ModelChecker::handle_simcall(Transition const& transition)
   s_mc_message_simcall_handle_t m;
   memset(&m, 0, sizeof(m));
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
-  m.pid   = transition.pid;
-  m.value = transition.argument;
+  m.pid   = transition.pid_;
+  m.value = transition.argument_;
   this->process_->get_channel().send(m);
   this->process_->clear_cache();
   if (this->process_->running())