do not load internal_config.h from mc.h

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index aadf44d..3f5864c 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -8,10 +8,6 @@
 
 #include <simgrid/modelchecker.h> /* our public interface (and definition of SIMGRID_HAVE_MC) */
 #include <simgrid/simix.h>
 
 #include <simgrid/modelchecker.h> /* our public interface (and definition of SIMGRID_HAVE_MC) */
 #include <simgrid/simix.h>

-#include <src/internal_config.h>
-#if HAVE_UCONTEXT_H
-#include <ucontext.h>           /* context relative declarations */
-#endif

 
 /* Maximum size of the application heap.
  *
 
 /* Maximum size of the application heap.
  *


@@ -66,15 +62,6 @@ XBT_PUBLIC(void) MC_process_clock_add(smx_actor_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_actor_t);
 XBT_PRIVATE void MC_automaton_load(const char *file);
 
 XBT_PUBLIC(double) MC_process_clock_get(smx_actor_t);
 XBT_PRIVATE void MC_automaton_load(const char *file);
 

-/****************************** MC ignore **********************************/
-XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
-XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size);
-XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame);
-XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name);
-#if HAVE_UCONTEXT_H
-XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_actor_t process, ucontext_t* context, size_t size);
-#endif
-

 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init();  /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit();
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init();  /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit();

diff --git a/src/kernel/context/Context.cpp b/src/kernel/context/Context.cpp
index 292ff2e..97b1985 100644 (file)
--- a/src/kernel/context/Context.cpp
+++ b/src/kernel/context/Context.cpp
@@ -1,21 +1,14 @@
-/* Copyright (c) 2007-2010, 2012-2015. The SimGrid Team.
- * All rights reserved.                                                     */
+/* Copyright (c) 2007-2017. 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. */
 
 
 /* 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 <cstdint>
-
-#include <memory>
-#include <functional>
-#include <utility>
-
-#include <simgrid/simix.hpp>
-

 #include "mc/mc.h"
 
 #include "src/kernel/context/Context.hpp"
 #include "src/simix/smx_private.h"
 #include "mc/mc.h"
 
 #include "src/kernel/context/Context.hpp"
 #include "src/simix/smx_private.h"

+#include "src/mc/mc_ignore.h"
+

 
 /**
  * @brief creates a new context for a user level process
 
 /**
  * @brief creates a new context for a user level process

diff --git a/src/kernel/context/ContextRaw.cpp b/src/kernel/context/ContextRaw.cpp
index 8ad2f11..5afc40f 100644 (file)
--- a/src/kernel/context/ContextRaw.cpp
+++ b/src/kernel/context/ContextRaw.cpp
@@ -1,22 +1,15 @@
-/* Copyright (c) 2009-2015. The SimGrid Team.
- * All rights reserved.                                                     */
+/* Copyright (c) 2009-2017. 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. */
 
 
 /* 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 <math.h>
-
-#include <utility>
-#include <functional>
-

 #include "src/internal_config.h" 
 
 #include "src/internal_config.h" 
 

-#include "xbt/log.h"

 #include "xbt/parmap.h"
 #include "xbt/parmap.h"

-#include "xbt/dynar.h"

 
 #include "src/simix/smx_private.h"
 #include "mc/mc.h"
 
 #include "src/simix/smx_private.h"
 #include "mc/mc.h"

+#include "src/mc/mc_ignore.h"

 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_context);
 
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_context);
 

diff --git a/src/kernel/context/ContextUnix.cpp b/src/kernel/context/ContextUnix.cpp
index f2f99a6..ac2a4b5 100644 (file)
--- a/src/kernel/context/ContextUnix.cpp
+++ b/src/kernel/context/ContextUnix.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2009-2015. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2009-2017. 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. */
 
 /* 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. */


@@ -7,10 +7,12 @@
 
 #include <ucontext.h>           /* context relative declarations */
 
 
 #include <ucontext.h>           /* context relative declarations */
 

-#include "mc/mc.h"

 #include "src/simix/ActorImpl.hpp"
 #include "src/simix/smx_private.h"
 #include "xbt/parmap.h"
 #include "src/simix/ActorImpl.hpp"
 #include "src/simix/smx_private.h"
 #include "xbt/parmap.h"

+#include "mc/mc.h"
+#include "src/mc/mc_ignore.h"
+

 
 /** Many integers are needed to store a pointer
  *
 
 /** Many integers are needed to store a pointer
  *

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 1a3a1a3..c80227d 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -3,34 +3,13 @@
 /* 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. */
 
 /* 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 <cassert>
-

 #include <simgrid_config.h>
 
 #include <simgrid_config.h>
 

-#include <xbt/log.h>
-#include <xbt/asserts.h>
-#include <xbt/dynar.h>
-
-#include <simgrid/simix.h>
-

 #include "mc/mc.h"
 #include "mc/mc.h"

-#include "src/mc/mc_base.h"

 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_replay.h"

-#include "src/mc/remote/mc_protocol.h"
-#include "src/simix/smx_private.h"
-
-#include "src/kernel/activity/ActivityImpl.hpp"
-#include "src/kernel/activity/SynchroIo.hpp"
-#include "src/kernel/activity/SynchroComm.hpp"
-#include "src/kernel/activity/SynchroRaw.hpp"
-#include "src/kernel/activity/SynchroSleep.hpp"
-#include "src/kernel/activity/SynchroExec.hpp"

 
 #if SIMGRID_HAVE_MC
 
 #if SIMGRID_HAVE_MC

-#include "src/mc/mc_request.h"
-#include "src/mc/Process.hpp"

 #include "src/mc/ModelChecker.hpp"
 #include "src/mc/ModelChecker.hpp"

-#include "src/mc/mc_smx.h"

 
 using simgrid::mc::remote;
 #endif
 
 using simgrid::mc::remote;
 #endif


@@ -41,9 +20,8 @@ int MC_random(int min, int max)
 {
 #if SIMGRID_HAVE_MC
   xbt_assert(mc_model_checker == nullptr);
 {
 #if SIMGRID_HAVE_MC
   xbt_assert(mc_model_checker == nullptr);

-  /* TODO, if the MC is disabled we do not really need to make a simcall for
-   * this :) */

 #endif
 #endif

+  /* TODO, if the MC is disabled we do not really need to make a simcall for this :) */

   return simcall_mc_random(min, max);
 }
 
   return simcall_mc_random(min, max);
 }
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 3d596ab..b3140e1 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -31,6 +31,7 @@
 #if SIMGRID_HAVE_MC
 #include <libunwind.h>
 #include "src/mc/mc_comm_pattern.h"
 #if SIMGRID_HAVE_MC
 #include <libunwind.h>
 #include "src/mc/mc_comm_pattern.h"

+#include "src/mc/mc_ignore.h"

 #include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_snapshot.h"
 #include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_snapshot.h"

diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
index b62bfb1..cf42fd1 100644 (file)
--- a/src/mc/mc_ignore.h
+++ b/src/mc/mc_ignore.h
@@ -6,12 +6,25 @@
 #ifndef SIMGRID_MC_IGNORE_H
 #define SIMGRID_MC_IGNORE_H
 
 #ifndef SIMGRID_MC_IGNORE_H
 #define SIMGRID_MC_IGNORE_H
 

-#include <xbt/base.h>           /* SG_BEGIN_DECL */
-#include <xbt/dynar.h>
+#include "src/internal_config.h"
+#include "xbt/dynar.h"
+
+#if HAVE_UCONTEXT_H
+#include <ucontext.h>           /* context relative declarations */
+#endif
+

 
 SG_BEGIN_DECL();
 
 
 SG_BEGIN_DECL();
 

-XBT_PRIVATE xbt_dynar_t MC_checkpoint_ignore_new(void);
+XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
+XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size);
+XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame);
+XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name);
+
+#if HAVE_UCONTEXT_H
+XBT_PUBLIC(void) MC_register_stack_area(void *stack, smx_actor_t process, ucontext_t* context, size_t size);
+#endif
+

 
 SG_END_DECL();
 
 
 SG_END_DECL();
 

diff --git a/src/mc/remote/Client.cpp b/src/mc/remote/Client.cpp
index 9759c21..b4a8aed 100644 (file)
--- a/src/mc/remote/Client.cpp
+++ b/src/mc/remote/Client.cpp
@@ -242,7 +242,7 @@ void Client::declareStack(void* stack, size_t size, smx_actor_t process, ucontex
   message.type         = MC_MESSAGE_STACK_REGION;
   message.stack_region = region;
   if (channel_.send(message))
   message.type         = MC_MESSAGE_STACK_REGION;
   message.stack_region = region;
   if (channel_.send(message))

-    xbt_die("Coule not send STACK_REGION to model-checker");
+    xbt_die("Could not send STACK_REGION to model-checker");

 }
 }
 }
 }
 }
 }

diff --git a/src/msg/instr_msg_task.cpp b/src/msg/instr_msg_task.cpp
index 65f32a6..fb6550f 100644 (file)
--- a/src/msg/instr_msg_task.cpp
+++ b/src/msg/instr_msg_task.cpp
@@ -7,6 +7,7 @@
 #include "mc/mc.h"
 #include "src/instr/instr_private.h"
 #include "src/msg/msg_private.h"
 #include "mc/mc.h"
 #include "src/instr/instr_private.h"
 #include "src/msg/msg_private.h"

+#include "src/mc/mc_ignore.h"

 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(instr_msg, instr, "MSG instrumentation");
 
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(instr_msg, instr, "MSG instrumentation");
 

diff --git a/src/msg/msg_global.cpp b/src/msg/msg_global.cpp
index 1eefcc5..0d94715 100644 (file)
--- a/src/msg/msg_global.cpp
+++ b/src/msg/msg_global.cpp
@@ -9,6 +9,7 @@
 #include "instr/instr_interface.h"
 #include "mc/mc.h"
 #include "src/msg/msg_private.h"
 #include "instr/instr_interface.h"
 #include "mc/mc.h"
 #include "src/msg/msg_private.h"

+#include "src/mc/mc_ignore.h"

 
 XBT_LOG_NEW_CATEGORY(msg, "All MSG categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(msg_kernel, msg, "Logging specific to MSG (kernel)");
 
 XBT_LOG_NEW_CATEGORY(msg, "All MSG categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(msg_kernel, msg, "Logging specific to MSG (kernel)");

diff --git a/src/smpi/smpi_process.cpp b/src/smpi/smpi_process.cpp
index 3d989e4..27bc512 100644 (file)
--- a/src/smpi/smpi_process.cpp
+++ b/src/smpi/smpi_process.cpp
@@ -4,6 +4,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "mc/mc.h"
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "mc/mc.h"

+#include "src/mc/mc_ignore.h"

 #include "src/mc/mc_replay.h"
 #include "src/msg/msg_private.h"
 #include "src/simix/smx_private.h"
 #include "src/mc/mc_replay.h"
 #include "src/msg/msg_private.h"
 #include "src/simix/smx_private.h"


@@ -12,6 +13,7 @@
 #include "src/smpi/smpi_group.hpp"
 #include "src/smpi/smpi_comm.hpp"
 
 #include "src/smpi/smpi_group.hpp"
 #include "src/smpi/smpi_comm.hpp"
 

+

 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_process, smpi, "Logging specific to SMPI (kernel)");
 
 //TODO : replace
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(smpi_process, smpi, "Logging specific to SMPI (kernel)");
 
 //TODO : replace

diff --git a/src/xbt/mmalloc/mfree.c b/src/xbt/mmalloc/mfree.c
index a08c7dd..5294c14 100644 (file)
--- a/src/xbt/mmalloc/mfree.c
+++ b/src/xbt/mmalloc/mfree.c
@@ -1,7 +1,6 @@
 /* Free a block of memory allocated by `mmalloc'. */
 
 /* Free a block of memory allocated by `mmalloc'. */
 

-/* Copyright (c) 2010-2015. The SimGrid Team.
- * All rights reserved.                                                     */
+/* Copyright (c) 2010-2017. 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. */
 
 /* 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. */


@@ -14,6 +13,7 @@
 #include "mmprivate.h"
 #include "xbt/ex.h"
 #include "mc/mc.h"
 #include "mmprivate.h"
 #include "xbt/ex.h"
 #include "mc/mc.h"

+#include "src/mc/mc_ignore.h"

 
 /* Return memory to the heap.
    Like `mfree' but don't call a mfree_hook if there is one.  */
 
 /* Return memory to the heap.
    Like `mfree' but don't call a mfree_hook if there is one.  */