[mc] Remove Process:status_

[simgrid.git] / src / mc / mc_global.cpp

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index ccda078..ab95c54 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -28,7 +28,7 @@
 #include "mc_record.h"
 
 #ifdef HAVE_MC
-#include "mc_server.h"
+#include "src/mc/Server.hpp"
 #include <libunwind.h>
 #include <xbt/mmalloc.h>
 #include "../xbt/mmalloc/mmprivate.h"
@@ -36,7 +36,6 @@
 #include "mc_comm_pattern.h"
 #include "mc_request.h"
 #include "mc_safety.h"
-#include "mc_memory_map.h"
 #include "mc_snapshot.h"
 #include "mc_liveness.h"
 #include "mc_private.h"
@@ -132,6 +131,9 @@ void MC_init_model_checker(pid_t pid, int socket)
 {
   mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
 
+  // TODO, avoid direct dependency on sg_cfg
+  mc_model_checker->process().privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
+
   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 
   /* Initialize statistics */
@@ -508,8 +510,10 @@ void MC_print_statistics(mc_stats_t stats)
     if (_sg_mc_comms_determinism)
       XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
   }
-  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS"))
-    system("free");
+  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
+    int ret=system("free");
+    if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
+  }
 }
 
 void MC_automaton_load(const char *file)
@@ -584,6 +588,25 @@ void MC_report_assertion_error(void)
   MC_print_statistics(mc_stats);
 }
 
+void MC_report_crash(int status)
+{
+  XBT_INFO("**************************");
+  XBT_INFO("** CRASH IN THE PROGRAM **");
+  XBT_INFO("**************************");
+  if (WIFSIGNALED(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.");
+  XBT_INFO("Counter-example execution trace:");
+  MC_record_dump_path(mc_stack);
+  MC_dump_stack_safety(mc_stack);
+  MC_print_statistics(mc_stats);
+}
+
 void MC_invalidate_cache(void)
 {
   if (mc_model_checker)