Merge branch 'master' of github.com:mquinson/simgrid

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

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index cccde0d..dfd9863 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -33,6 +33,16 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
 namespace simgrid {
 namespace mc {
 
+static void MC_show_non_termination(void)
+{
+  XBT_INFO("******************************************");
+  XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+  XBT_INFO("******************************************");
+  XBT_INFO("Counter-example execution trace:");
+  MC_dump_stack_safety(mc_stack);
+  MC_print_statistics(mc_stats);
+}
+
 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;
@@ -150,7 +160,7 @@ int SafetyChecker::run()
 
       /* Check for deadlocks */
       if (mc_model_checker->checkDeadlock()) {
-        MC_show_deadlock(nullptr);
+        MC_show_deadlock();
         return SIMGRID_MC_EXIT_DEADLOCK;
       }