[pvs] Expression 'req' is always true.

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

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 70cf3989553e1e70cb00e28a95db3dbac8306574..feb44630646dc1d2bd43af8ebcae1f43eab0e7ec 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -63,8 +63,7 @@ std::vector<std::string> SafetyChecker::get_textual_trace() // override
   for (auto const& state : stack_) {
     int value         = state->transition_.argument_;
     smx_simcall_t req = &state->executed_req_;
-    if (req)
-      trace.push_back(request_to_string(req, value, RequestType::executed));
+    trace.push_back(request_to_string(req, value, RequestType::executed));
   }
   return trace;
 }
@@ -135,7 +134,8 @@ void SafetyChecker::run()
     this->get_session().execute(state->transition_);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
-    std::unique_ptr<State> next_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+    ++expanded_states_count_;
+    auto next_state = std::make_unique<State>(expanded_states_count_);
 
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
@@ -147,7 +147,7 @@ void SafetyChecker::run()
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {
       /* Get an enabled process and insert it in the interleave set of the next state */
-      for (auto& remoteActor : mc_model_checker->process().actors()) {
+      for (auto& remoteActor : mc_model_checker->get_remote_simulation().actors()) {
         auto actor = remoteActor.copy.get_buffer();
         if (actor_is_enabled(actor)) {
           next_state->add_interleaving_set(actor);
@@ -191,7 +191,7 @@ void SafetyChecker::backtrack()
     stack_.pop_back();
     if (reductionMode_ == ReductionMode::dpor) {
       smx_simcall_t req = &state->internal_req_;
-      if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
+      if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK)
         xbt_die("Mutex is currently not supported with DPOR,  use --cfg=model-check/reduction:none");
 
       const kernel::actor::ActorImpl* issuer = MC_smx_simcall_get_issuer(req);
@@ -246,7 +246,7 @@ void SafetyChecker::restore_state()
   /* Intermediate backtracking */
   const State* last_state = stack_.back().get();
   if (last_state->system_state_) {
-    last_state->system_state_->restore(&mc_model_checker->process());
+    last_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
     return;
   }
 
@@ -282,13 +282,14 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s)
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  std::unique_ptr<State> initial_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+  ++expanded_states_count_;
+  auto initial_state = std::make_unique<State>(expanded_states_count_);
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
 
   /* Get an enabled actor and insert it in the interleave set of the initial state */
-  for (auto& actor : mc_model_checker->process().actors())
+  for (auto& actor : mc_model_checker->get_remote_simulation().actors())
     if (actor_is_enabled(actor.copy.get_buffer())) {
       initial_state->add_interleaving_set(actor.copy.get_buffer());
       if (reductionMode_ != ReductionMode::none)