let model-checking compile without supernovae activated, too

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 70fa118..dd6761c 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -336,7 +336,6 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
-
 /**
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f4e5499..9a0ee71 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -267,5 +267,10 @@ void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
 void MC_pair_stateless_delete(mc_pair_stateless_t pair);
 
+/********************************** Configuration of MC **************************************/
+
+extern int _surf_do_mc_checkpoint;
+extern xbt_fifo_t mc_stack_safety;
+
 
 #endif