[mc] Cleanup safety initialisation code

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index da02e1d..53235a4 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -5,6 +5,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include <string.h>
+#include <stdint.h>
 
 #include "mc_base.h"
 
@@ -283,26 +284,24 @@ void MC_do_the_modelcheck_for_real()
   }
 
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
-    if(_sg_mc_termination){
-      XBT_INFO("Check non progressive cycles");
+    if(_sg_mc_termination)
       mc_reduce_kind = e_mc_reduce_none;
-    } else {
-      if (mc_reduce_kind == e_mc_reduce_unset)
-        mc_reduce_kind = e_mc_reduce_dpor;
-      else {
-        _sg_mc_safety = 1;
-        mc_reduce_kind = e_mc_reduce_dpor;
-        if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
-          XBT_INFO("Check a safety property");
-          MC_modelcheck_safety();
-        }
-        else {
-          // Most of this is not needed:
-          MC_init();
-          // Main event loop:
-          MC_client_main_loop();
-        }
-      }
+    else if (mc_reduce_kind == e_mc_reduce_unset)
+      mc_reduce_kind = e_mc_reduce_dpor;
+    _sg_mc_safety = 1;
+    if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+      if (_sg_mc_termination)
+        XBT_INFO("Check non progressive cycles");
+      else
+        XBT_INFO("Check a safety property");
+      MC_wait_for_requests();
+      MC_modelcheck_safety();
+    }
+    else {
+      // Most of this is not needed:
+      MC_init();
+      // Main event loop:
+      MC_client_main_loop();
     }
   }
 
@@ -785,7 +784,16 @@ void MC_dump_stacks(FILE* file)
     unw_word_t off;
     do {
       const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";
+#if defined(__x86_64__)
+      unw_word_t rip = 0;
+      unw_word_t rsp = 0;
+      unw_get_reg(&c, UNW_X86_64_RIP, &rip);
+      unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
+      fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
+        nframe, name, rip, rsp);
+#else
       fprintf(file, "  %i: %s\n", nframe, name);
+#endif
       ++nframe;
     } while(unw_step(&c));