cosmetics

diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index 0579ca6..a097953 100644 (file)
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -31,10 +31,10 @@ XBT_PUBLIC(int) MC_random(int min, int max);
  *
  * Please don't use directly: you should use MC_is_active. */
 extern XBT_PUBLIC(int) _sg_do_model_check;
-extern XBT_PUBLIC(int) _sg_mc_visited;
+extern XBT_PUBLIC(int) _sg_mc_max_visited_states;
 
 #define MC_is_active()                  _sg_do_model_check
-#define MC_visited_reduction()          _sg_mc_visited
+#define MC_visited_reduction() _sg_mc_max_visited_states
 
 /** Assertion for the model-checker
  *

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 39213e1..2d37e15 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -39,7 +39,7 @@ extern XBT_PUBLIC(char*) _sg_mc_property_file;
 extern XBT_PRIVATE int _sg_mc_timeout;
 extern XBT_PRIVATE int _sg_mc_hash;
 extern XBT_PRIVATE int _sg_mc_max_depth;
-extern XBT_PUBLIC(int) _sg_mc_visited;
+extern XBT_PUBLIC(int) _sg_mc_max_visited_states;
 extern XBT_PRIVATE char* _sg_mc_dot_output_file;
 extern XBT_PUBLIC(int) _sg_mc_comms_determinism;
 extern XBT_PUBLIC(int) _sg_mc_send_determinism;

diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index a109f83..07f510c 100644 (file)
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -147,7 +147,7 @@ public:
       this->refresh_heap();
     return this->heap.get();
   }
-  malloc_info* get_malloc_info()
+  const malloc_info* get_malloc_info()
   {
     if (!(this->cache_flags_ & Process::cache_malloc))
       this->refresh_malloc_info();

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index c57bf9c..a2348a8 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -60,7 +60,7 @@ VisitedState::~VisitedState()
 
 void VisitedStates::prune()
 {
-  while (states_.size() > (std::size_t) _sg_mc_visited) {
+  while (states_.size() > (std::size_t)_sg_mc_max_visited_states) {
     XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
     auto min_element = boost::range::min_element(states_,
       [](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index fa5ab40..e899990 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -512,9 +512,9 @@ void CommunicationDeterminismChecker::main(void)
       bool compare_snapshots = all_communications_are_finished()
         && this->initial_communications_pattern_done;
 
-      if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(
-            expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
+      if (_sg_mc_max_visited_states == 0 ||
+          (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
+              nullptr) {
 
         /* Get enabled actors and insert them in the interleave set of the next state */
         for (auto& actor : mc_model_checker->process().actors())

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index a28aa51..a505e09 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -220,7 +220,7 @@ void LivenessChecker::replay()
  */
 int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair)
 {
-  if (_sg_mc_visited == 0)
+  if (_sg_mc_max_visited_states == 0)
     return -1;
 
   if (visited_pair == nullptr)
@@ -258,7 +258,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
 
 void LivenessChecker::purgeVisitedPairs()
 {
-  if (_sg_mc_visited != 0 && visitedPairs_.size() > (std::size_t) _sg_mc_visited) {
+  if (_sg_mc_max_visited_states != 0 && visitedPairs_.size() > (std::size_t)_sg_mc_max_visited_states) {
     // Remove the oldest entry with a linear search:
     visitedPairs_.erase(boost::min_element(visitedPairs_,
       [](std::shared_ptr<VisitedPair> const a, std::shared_ptr<VisitedPair> const& b) {

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 52e1e70..2185577 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -158,7 +158,7 @@ void SafetyChecker::run()
       this->checkNonTermination(next_state.get());
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
-    if (_sg_mc_visited == true)
+    if (_sg_mc_max_visited_states == true)
       visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
 
     /* If this is a new state (or if we don't care about state-equality reduction) */

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index f5530bd..e6e2a77 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -113,8 +113,8 @@ bool request_is_enabled(smx_simcall_t req)
 #if HAVE_MC
     // Fetch from MCed memory:
     // HACK, type puning
-    simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
     if (mc_model_checker != nullptr) {
+      simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
       mc_model_checker->process().read(temp_comm, remote(act));
       act = static_cast<simgrid::kernel::activity::Comm*>(temp_comm.getBuffer());
     }

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 6deee1c..3716919 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -578,7 +578,7 @@ std::shared_ptr<simgrid::mc::Snapshot> take_snapshot(int num_state)
 
   snapshot->to_ignore = mc_model_checker->process().ignored_heap();
 
-  if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
+  if (_sg_mc_max_visited_states > 0 || strcmp(_sg_mc_property_file, "")) {
     snapshot->stacks = take_snapshot_stacks(snapshot.get());
     if (_sg_mc_hash)
       snapshot->hash = simgrid::mc::hash(*snapshot);

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 84b8b07..67bebd4 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -55,7 +55,7 @@ int _sg_mc_ksm = 0;
 char *_sg_mc_property_file = nullptr;
 int _sg_mc_hash = 0;
 int _sg_mc_max_depth = 1000;
-int _sg_mc_visited = 0;
+int _sg_mc_max_visited_states = 0;
 char *_sg_mc_dot_output_file = nullptr;
 int _sg_mc_comms_determinism = 0;
 int _sg_mc_send_determinism = 0;
@@ -144,7 +144,7 @@ void _mc_cfg_cb_visited(const char *name)
     xbt_die
         ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
 
-  _sg_mc_visited = xbt_cfg_get_int(name);
+  _sg_mc_max_visited_states = xbt_cfg_get_int(name);
 }
 
 void _mc_cfg_cb_dot_output(const char *name)

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 861e399..e85574f 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -165,11 +165,10 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   if (!req)
     return nullptr;
 
-  // Fetch the data of the request and translate it:
-
   state->transition.pid = process->pid;
-
   state->executed_req = *req;
+  // Fetch the data of the request and translate it:
+  state->internal_req = *req;
 
   /* The waitany and testany request are transformed into a wait or test request
    * over the corresponding communication action so it can be treated later by
@@ -177,7 +176,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   switch (req->call) {
   case SIMCALL_COMM_WAITANY: {
     state->internal_req.call = SIMCALL_COMM_WAIT;
-    state->internal_req.issuer = req->issuer;
     smx_activity_t remote_comm;
     read_element(mc_model_checker->process(),
       &remote_comm, remote(simcall_comm_waitany__get__comms(req)),
@@ -191,7 +189,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
 
   case SIMCALL_COMM_TESTANY:
     state->internal_req.call = SIMCALL_COMM_TEST;
-    state->internal_req.issuer = req->issuer;
 
     if (state->transition.argument > 0) {
       smx_activity_t remote_comm = mc_model_checker->process().read(
@@ -205,7 +202,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     break;
 
   case SIMCALL_COMM_WAIT:
-    state->internal_req = *req;
     mc_model_checker->process().read_bytes(&state->internal_comm ,
       sizeof(state->internal_comm), remote(simcall_comm_wait__get__comm(req)));
     simcall_comm_wait__set__comm(&state->executed_req, state->internal_comm.getBuffer());
@@ -213,7 +209,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     break;
 
   case SIMCALL_COMM_TEST:
-    state->internal_req = *req;
     mc_model_checker->process().read_bytes(&state->internal_comm,
       sizeof(state->internal_comm), remote(simcall_comm_test__get__comm(req)));
     simcall_comm_test__set__comm(&state->executed_req, state->internal_comm.getBuffer());
@@ -221,7 +216,7 @@ static inline smx_simcall_t MC_state_get_request_for_process(
     break;
 
   default:
-    state->internal_req = *req;
+    /* No translation needed */
     break;
   }