[mc] Move MC_important_snapshot() as a method of ModelChecker

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 2e72956..f8b0982 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -52,6 +52,11 @@ public:
     return page_store_;
   }
   const char* get_host_name(const char* name);
     return page_store_;
   }
   const char* get_host_name(const char* name);

+
+  bool is_important_snapshot(Snapshot const& snapshot) const
+  {
+    return &snapshot == mc_model_checker->parent_snapshot_;
+  }

 };
 
 }
 };
 
 }

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index aadcea8..763e116 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -50,18 +50,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
 /************************************  Free functions **************************************/
 /*****************************************************************************************/
 
 /************************************  Free functions **************************************/
 /*****************************************************************************************/
 

-int MC_important_snapshot(mc_snapshot_t snapshot)
-{
-  // We need this snapshot in order to know which
-  // pages needs to be stored in the next snapshot.
-  // This field is only non-NULL when using soft-dirty
-  // page tracking.
-  if (snapshot == mc_model_checker->parent_snapshot_)
-    return true;
-
-  return false;
-}
-

 /** @brief Restore a region from a snapshot
  *
  *  @param reg     Target region
 /** @brief Restore a region from a snapshot
  *
  *  @param reg     Target region

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f88c5c4..bbd2a64 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -118,8 +118,6 @@ XBT_PRIVATE void MC_report_assertion_error(void);
 
 XBT_PRIVATE void MC_invalidate_cache(void);
 
 
 XBT_PRIVATE void MC_invalidate_cache(void);
 

-XBT_PRIVATE int MC_important_snapshot(mc_snapshot_t snapshot);
-

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index e8e6922..40db5aa 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -355,7 +355,8 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 
       mc_visited_state_t state_test;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
 
       mc_visited_state_t state_test;
       xbt_dynar_foreach(visited_states, cursor2, state_test){

-        if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
+        if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
+            && state_test->num < min2) {

           index2 = cursor2;
           min2 = state_test->num;
         }
           index2 = cursor2;
           min2 = state_test->num;
         }


@@ -472,7 +473,7 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {

-        if (!MC_important_snapshot(pair_test->graph_state->system_state)
+        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)

             && pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;
             && pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;