[mc] Dummy SafetyChecker class

diff --git a/src/mc/mc_safety.cpp b/src/mc/SafetyChecker.cpp
similarity index 97%
rename from src/mc/mc_safety.cpp
rename to src/mc/SafetyChecker.cpp
index 4b214ff..b37bf5f 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2015. The SimGrid Team.
+/* Copyright (c) 2016. The SimGrid Team.

  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it


@@ -22,6 +22,8 @@
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/mc_smx.h"
 #include "src/mc/Client.hpp"
 #include "src/mc/mc_exit.h"

+#include "src/mc/Checker.hpp"
+#include "src/mc/SafetyChecker.hpp"

 
 #include "src/xbt/mmalloc/mmprivate.h"
 
 
 #include "src/xbt/mmalloc/mmprivate.h"
 


@@ -77,7 +79,7 @@ static void pre_modelcheck_safety()
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */

-int modelcheck_safety(void)
+static int modelcheck_safety(void)

 {
   modelcheck_safety_init();
 
 {
   modelcheck_safety_init();
 


@@ -284,5 +286,18 @@ static void modelcheck_safety_init(void)
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 }
 
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 }
 

+SafetyChecker::SafetyChecker(Session& session) : Checker(session)
+{
+}
+
+SafetyChecker::~SafetyChecker()
+{
+}
+
+int SafetyChecker::run()
+{
+  return simgrid::mc::modelcheck_safety();
+}
+  

 }
 }
 }
 }

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
new file mode 100644 (file)
index 0000000..597af14
--- /dev/null
+++ b/src/mc/SafetyChecker.hpp
@@ -0,0 +1,26 @@
+/* Copyright (c) 2008-2016. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
+#define SIMGRID_MC_SAFETY_CHECKER_HPP
+
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/Checker.hpp"
+
+namespace simgrid {
+namespace mc {
+
+class SafetyChecker : public Checker {
+public:
+  SafetyChecker(Session& session);
+  ~SafetyChecker();
+  int run() override;
+};
+
+}
+}
+
+#endif

diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h
index 25eb06a..8e7503f 100644 (file)
--- a/src/mc/mc_safety.h
+++ b/src/mc/mc_safety.h
@@ -31,8 +31,6 @@ enum class ReductionMode {
 
 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
 
 
 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
 

-int modelcheck_safety(void);
-

 struct XBT_PRIVATE VisitedState {
   simgrid::mc::Snapshot* system_state = nullptr;
   size_t heap_bytes_used = 0;
 struct XBT_PRIVATE VisitedState {
   simgrid::mc::Snapshot* system_state = nullptr;
   size_t heap_bytes_used = 0;

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index e153b0c..3d3017d 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -28,6 +28,7 @@
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"

+#include "src/mc/SafetyChecker.hpp"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 


@@ -51,8 +52,8 @@ std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session& sessio
     code = [](Session& session) {
       return MC_modelcheck_comm_determinism(); };
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
     code = [](Session& session) {
       return MC_modelcheck_comm_determinism(); };
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')

-    code = [](Session& session) {
-      return simgrid::mc::modelcheck_safety(); };
+    return std::unique_ptr<simgrid::mc::Checker>(
+      new simgrid::mc::SafetyChecker(session));

   else
     code = [](Session& session) {
       return simgrid::mc::modelcheck_liveness(); };
   else
     code = [](Session& session) {
       return simgrid::mc::modelcheck_liveness(); };

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 989aa3c..b7f6cfb 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -562,6 +562,8 @@ set(MC_SRC
   src/mc/ObjectInformation.cpp
   src/mc/PageStore.hpp
   src/mc/PageStore.cpp
   src/mc/ObjectInformation.cpp
   src/mc/PageStore.hpp
   src/mc/PageStore.cpp

+  src/mc/SafetyChecker.cpp
+  src/mc/SafetyChecker.hpp

   src/mc/ChunkedData.hpp
   src/mc/ChunkedData.cpp
   src/mc/RegionSnapshot.cpp
   src/mc/ChunkedData.hpp
   src/mc/ChunkedData.cpp
   src/mc/RegionSnapshot.cpp


@@ -608,7 +610,6 @@ set(MC_SRC
   src/mc/mc_request.h
   src/mc/mc_request.cpp
   src/mc/mc_safety.h
   src/mc/mc_request.h
   src/mc/mc_request.cpp
   src/mc/mc_safety.h

-  src/mc/mc_safety.cpp

   src/mc/mc_state.h
   src/mc/mc_state.cpp
   src/mc/mc_visited.cpp
   src/mc/mc_state.h
   src/mc/mc_state.cpp
   src/mc/mc_visited.cpp