[mc] Move some MC_show_non_termination() in SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 3989b92..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 {
 
 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;
 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 4cd9edd..24d755c 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -247,15 +247,6 @@ void MC_show_deadlock(void)
   MC_print_statistics(mc_stats);
 }
 
   MC_print_statistics(mc_stats);
 }
 

-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);
-}
-

 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {
 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 57f6746..3696409 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -68,7 +68,6 @@ XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
 XBT_PRIVATE void MC_show_deadlock(void);
 XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
 XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);
 XBT_PRIVATE void MC_show_deadlock(void);
 XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
 XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);

-XBT_PRIVATE void MC_show_non_termination(void);

 
 /** Stack (of `mc_state_t`) representing the current position of the
  *  the MC in the exploration graph
 
 /** Stack (of `mc_state_t`) representing the current position of the
  *  the MC in the exploration graph