Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
kill some dead code
[simgrid.git] / src / mc / mc_safety.cpp
index 74fde12..4b214ff 100644 (file)
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
 #include "src/mc/mc_exit.h"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
-extern "C" {
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
-}
-
 namespace simgrid {
 namespace mc {
 
@@ -56,8 +52,7 @@ static void modelcheck_safety_init(void);
  */
 static void pre_modelcheck_safety()
 {
-  if (_sg_mc_visited > 0)
-    simgrid::mc::visited_states = simgrid::xbt::newDeleteDynar<simgrid::mc::VisitedState>();
+  simgrid::mc::visited_states.clear();
 
   mc_state_t initial_state = MC_state_new();
 
@@ -91,7 +86,7 @@ int modelcheck_safety(void)
   smx_simcall_t req = nullptr;
   mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
   xbt_fifo_item_t item = nullptr;
-  simgrid::mc::VisitedState* visited_state = nullptr;
+  std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 
   while (xbt_fifo_size(mc_stack) > 0) {
 
@@ -184,7 +179,7 @@ int modelcheck_safety(void)
       visited_state = nullptr;
 
       /* Check for deadlocks */
-      if (MC_deadlock_check()) {
+      if (mc_model_checker->checkDeadlock()) {
         MC_show_deadlock(nullptr);
         return SIMGRID_MC_EXIT_DEADLOCK;
       }