MC: inline a function that is now trivial

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index faaf181..87ed0f5 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -101,7 +101,7 @@ void Session::initialize()
 {
   xbt_assert(initial_snapshot_ == nullptr);
   mc_model_checker->wait_for_requests();
-  initial_snapshot_ = simgrid::mc::take_snapshot(0);
+  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
 }
 
 void Session::execute(Transition const& transition)

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 5e4f99c..2d39ded 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -33,7 +33,7 @@ VisitedState::VisitedState(unsigned long state_number) : num(state_number)
 
   this->actors_count = mc_model_checker->process().actors().size();
 
-  this->system_state = simgrid::mc::take_snapshot(state_number);
+  this->system_state = std::make_shared<simgrid::mc::Snapshot>(state_number);
   this->original_num = -1;
 }
 

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index e04712b..4638611 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -30,7 +30,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
 
   this->graph_state = std::move(graph_state);
   if(this->graph_state->system_state == nullptr)
-    this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
+    this->graph_state->system_state = std::make_shared<simgrid::mc::Snapshot>(pair_num);
   this->heap_bytes_used = mmalloc_get_bytes_used_remote(process->get_heap()->heaplimit, process->get_malloc_info());
 
   this->actors_count = mc_model_checker->process().actors().size();

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 4ad61ab..542163b 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -27,7 +27,7 @@ State::State(unsigned long state_number) : num(state_number)
   actorStates.resize(MC_smx_get_maxpid());
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
-    system_state = simgrid::mc::take_snapshot(num);
+    system_state = std::make_shared<simgrid::mc::Snapshot>(num);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
       MC_state_copy_incomplete_communications_pattern(this);
       MC_state_copy_index_communications_pattern(this);

diff --git a/src/mc/sosp/mc_checkpoint.cpp b/src/mc/sosp/mc_checkpoint.cpp
index c300c47..24f38d6 100644 (file)
--- a/src/mc/sosp/mc_checkpoint.cpp
+++ b/src/mc/sosp/mc_checkpoint.cpp
@@ -96,14 +96,5 @@ void find_object_address(std::vector<simgrid::xbt::VmMap> const& maps, simgrid::
   xbt_assert(result->start_exec || result->start_rw || result->start_ro);
 }
 
-
-std::shared_ptr<simgrid::mc::Snapshot> take_snapshot(int num_state)
-{
-  XBT_DEBUG("Taking snapshot %i", num_state);
-
-  std::shared_ptr<simgrid::mc::Snapshot> snapshot = std::make_shared<simgrid::mc::Snapshot>(num_state);
-  return snapshot;
-}
-
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/sosp/mc_snapshot.cpp b/src/mc/sosp/mc_snapshot.cpp
index 97341f6..1a61f33 100644 (file)
--- a/src/mc/sosp/mc_snapshot.cpp
+++ b/src/mc/sosp/mc_snapshot.cpp
@@ -273,13 +273,15 @@ static void snapshot_ignore_restore(simgrid::mc::Snapshot* snapshot)
     snapshot->process()->write_bytes(ignored_data.data.data(), ignored_data.data.size(), remote(ignored_data.start));
 }
 
-Snapshot::Snapshot(int _num_state, RemoteClient* process)
+Snapshot::Snapshot(int num_state, RemoteClient* process)
     : AddressSpace(process)
-    , num_state_(_num_state)
+    , num_state_(num_state)
     , heap_bytes_used_(0)
     , enabled_processes_()
     , hash_(0)
 {
+  XBT_DEBUG("Taking snapshot %i", num_state);
+
   for (auto const& p : process->actors())
     enabled_processes_.insert(p.copy.get_buffer()->get_pid());
 

diff --git a/src/mc/sosp/mc_snapshot.hpp b/src/mc/sosp/mc_snapshot.hpp
index 11496c2..c0e44d6 100644 (file)
--- a/src/mc/sosp/mc_snapshot.hpp
+++ b/src/mc/sosp/mc_snapshot.hpp
@@ -101,13 +101,6 @@ private:
 
 static const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot);
 
-namespace simgrid {
-namespace mc {
-
-XBT_PRIVATE std::shared_ptr<Snapshot> take_snapshot(int num_state);
-} // namespace mc
-} // namespace simgrid
-
 const void* MC_region_read_fragmented(simgrid::mc::RegionSnapshot* region, void* target, const void* addr,
                                       std::size_t size);