Fix segfault with debug message.

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

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index cefde1f..892f173 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -3,16 +3,7 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#include <cassert>
-#include <cstdio>
-
-#include <memory>
-#include <string>
-#include <vector>
-
-#include <xbt/log.h>
-#include <xbt/sysdep.h>
-
+#include "src/mc/Session.hpp"
 #include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/SafetyChecker.hpp"
@@ -20,9 +11,17 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
-#include "src/mc/mc_request.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
+#include "xbt/log.h"
+#include "xbt/sysdep.h"
+
+#include <cassert>
+#include <cstdio>
+
+#include <memory>
+#include <string>
+#include <vector>
 
 using api = simgrid::mc::Api;
 
@@ -113,6 +112,7 @@ void SafetyChecker::run()
     if (req == nullptr) {
       XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
 
+//      mc_model_checker->finalize_app();
       this->backtrack();
       continue;
     }
@@ -147,7 +147,7 @@ void SafetyChecker::run()
       auto actors = api::get().get_actors(); 
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
-        if (api::get().actor_is_enabled(actor->get_pid())) {
+        if (get_session().actor_is_enabled(actor->get_pid())) {
           next_state->mark_todo(actor);
           if (reductionMode_ == ReductionMode::dpor)
             break; // With DPOR, we take the first enabled transition
@@ -185,7 +185,7 @@ void SafetyChecker::backtrack()
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
       auto call = state->executed_req_.call_;
-      const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
+      kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_);
       for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
         State* prev_state = i->get();
         if (state->executed_req_.issuer_ == prev_state->executed_req_.issuer_) {
@@ -206,7 +206,7 @@ void SafetyChecker::backtrack()
           if (not prev_state->actor_states_[issuer->get_pid()].is_done())
             prev_state->mark_todo(issuer);
           else
-            XBT_DEBUG("Actor %s %ld is in done set", issuer->get_cname(), issuer->get_pid());
+            XBT_DEBUG("Actor %s %ld is in done set", api::get().get_actor_name(issuer).c_str(), issuer->get_pid());
           break;
         } else {
           const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->executed_req_);
@@ -239,8 +239,7 @@ void SafetyChecker::restore_state()
     return;
   }
 
-  /* Restore the initial state */
-  api::get().restore_initial_state();
+  get_session().restore_initial_state();
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (std::unique_ptr<State> const& state : stack_) {
@@ -267,8 +266,8 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
     XBT_INFO("Check a safety property. Reduction is: %s.",
              (reductionMode_ == ReductionMode::none ? "none"
                                                     : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
-  
-  api::get().session_initialize();  
+
+  get_session().take_initial_snapshot();
 
   XBT_DEBUG("Starting the safety algorithm");
 
@@ -281,7 +280,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   auto actors = api::get().get_actors();
   for (auto& actor : actors)
-    if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
+    if (get_session().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
       initial_state->mark_todo(actor.copy.get_buffer());
       if (reductionMode_ != ReductionMode::none)
         break;