Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[pvs] Expression 'req' is always true.
authorArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Wed, 25 Nov 2020 21:55:46 +0000 (22:55 +0100)
committerArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Wed, 25 Nov 2020 21:55:46 +0000 (22:55 +0100)
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp

index e90478f..4022f90 100644 (file)
@@ -297,8 +297,7 @@ std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() //
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
     smx_simcall_t req = &state->executed_req_;
-    if (req)
-      trace.push_back(request_to_string(req, state->transition_.argument_, RequestType::executed));
+    trace.push_back(request_to_string(req, state->transition_.argument_, RequestType::executed));
   }
   return trace;
 }
index f644c90..377c3aa 100644 (file)
@@ -144,16 +144,14 @@ void LivenessChecker::replay()
 
       smx_simcall_t req = nullptr;
 
-      if (saved_req != nullptr) {
-        /* because we got a copy of the executed request, we have to fetch the
-             real one, pointed by the request field of the issuer process */
-        const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
-        req                      = &issuer->simcall_;
-
-        /* Debug information */
-        XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                  request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
-      }
+      /* because we got a copy of the executed request, we have to fetch the
+         real one, pointed by the request field of the issuer process */
+      const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+      req                      = &issuer->simcall_;
+
+      /* Debug information */
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
+                request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
 
       this->get_session().execute(state->transition_);
     }
@@ -253,7 +251,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
   for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
     int req_num       = pair->graph_state->transition_.argument_;
     smx_simcall_t req = &pair->graph_state->executed_req_;
-    if (req && req->call_ != simix::Simcall::NONE)
+    if (req->call_ != simix::Simcall::NONE)
       trace.push_back(request_to_string(req, req_num, RequestType::executed));
   }
   return trace;
index 6284972..feb4463 100644 (file)
@@ -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;
 }