From 362b4dbfe18e585af36789119acafa5d5350fa20 Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@loria.fr>
Date: Wed, 8 Feb 2012 16:54:16 +0100
Subject: [PATCH] move a public header in the simgrid/ directory to fight the
 namespace polution

---
 examples/msg/chord/chord.c         |  3 +--
 examples/msg/mc/bugged1.c          |  2 +-
 examples/msg/mc/bugged1_stateful.c |  4 ++--
 examples/msg/mc/bugged2.c          |  2 +-
 examples/msg/mc/bugged2_stateful.c |  2 +-
 examples/msg/mc/bugged3.c          |  2 +-
 examples/msg/mc/random_test.c      |  2 +-
 include/mc/modelchecker.h          |  6 ------
 include/simgrid/modelchecker.h     | 27 +++++++++++++++++++++++++++
 9 files changed, 35 insertions(+), 15 deletions(-)
 delete mode 100644 include/mc/modelchecker.h
 create mode 100644 include/simgrid/modelchecker.h

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index f6ce033da1..de95ba8c02 100644
--- a/examples/msg/chord/chord.c
+++ b/examples/msg/chord/chord.c
@@ -9,8 +9,7 @@
 #include "msg/msg.h"
 #include "xbt/log.h"
 #include "xbt/asserts.h"
-#include "mc/modelchecker.h"
-#include "mc/mc.h"
+#include "simgrid/modelchecker.h"
 #include "xbt/xbt_os_time.h"
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord,
diff --git a/examples/msg/mc/bugged1.c b/examples/msg/mc/bugged1.c
index 16425d7c63..80fbae2723 100644
--- a/examples/msg/mc/bugged1.c
+++ b/examples/msg/mc/bugged1.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
diff --git a/examples/msg/mc/bugged1_stateful.c b/examples/msg/mc/bugged1_stateful.c
index cb4ec29fe8..4bf0381230 100644
--- a/examples/msg/mc/bugged1_stateful.c
+++ b/examples/msg/mc/bugged1_stateful.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
@@ -62,4 +62,4 @@ int main(int argc, char *argv[])
    
   return 0;
 
-}
\ No newline at end of file
+}
diff --git a/examples/msg/mc/bugged2.c b/examples/msg/mc/bugged2.c
index 95c08544e3..28ef0f7a5f 100644
--- a/examples/msg/mc/bugged2.c
+++ b/examples/msg/mc/bugged2.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
diff --git a/examples/msg/mc/bugged2_stateful.c b/examples/msg/mc/bugged2_stateful.c
index 6b4597d6c9..8c6df80f40 100644
--- a/examples/msg/mc/bugged2_stateful.c
+++ b/examples/msg/mc/bugged2_stateful.c
@@ -4,7 +4,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
diff --git a/examples/msg/mc/bugged3.c b/examples/msg/mc/bugged3.c
index 8e33b31fa1..0a21025cce 100644
--- a/examples/msg/mc/bugged3.c
+++ b/examples/msg/mc/bugged3.c
@@ -8,7 +8,7 @@
 /******************************************************************************/
 
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "this example");
 
diff --git a/examples/msg/mc/random_test.c b/examples/msg/mc/random_test.c
index c7e474dc83..9dda26d5f8 100644
--- a/examples/msg/mc/random_test.c
+++ b/examples/msg/mc/random_test.c
@@ -1,5 +1,5 @@
 #include <msg/msg.h>
-#include <mc/modelchecker.h>
+#include <simgrid/modelchecker.h>
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(random_test, "Random Test");
 
diff --git a/include/mc/modelchecker.h b/include/mc/modelchecker.h
deleted file mode 100644
index 087692b4ac..0000000000
--- a/include/mc/modelchecker.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#include "xbt.h"
-
-XBT_PUBLIC(void) MC_assert(int);
-XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(int) MC_random(int min, int max);
-XBT_PUBLIC(void) MC_diff();
diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
new file mode 100644
index 0000000000..b0d7a37042
--- /dev/null
+++ b/include/simgrid/modelchecker.h
@@ -0,0 +1,27 @@
+/* simgrid/modelchecker.h - Formal Verification made possible in SimGrid    */
+
+/* Copyright (c) 2008-2012. 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. */
+
+#include <simgrid_config.h> /* HAVE_MC ? */
+#include <xbt.h>
+
+#ifndef SIMGRID_MODELCHECKER_H
+#define SIMGRID_MODELCHECKER_H
+
+#ifdef HAVE_MC
+extern int _surf_do_model_check;
+#define MC_IS_ENABLED _surf_do_model_check
+#else
+#define MC_IS_ENABLED 0
+#endif
+
+
+XBT_PUBLIC(void) MC_assert(int);
+XBT_PUBLIC(void) MC_assert_stateful(int);
+XBT_PUBLIC(int) MC_random(int min, int max);
+XBT_PUBLIC(void) MC_diff();
+
+#endif /* SIMGRID_MODELCHECKER_H */
-- 
2.20.1