[mc] Remove useless header #includes

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index d205926..8680749 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -14,6 +14,7 @@
 #include <dirent.h>
 
 #include "internal_config.h"
+#include "mc_memory_map.h"
 #include "mc_private.h"
 #include "xbt/module.h"
 #include <xbt/mmalloc.h>
@@ -31,6 +32,8 @@
 #include "mc_private.h"
 #include <mc/mc.h>
 
+#include "mc_snapshot.h"
+#include "mc_object_info.h"
 #include "mc_mmu.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,

diff --git a/src/mc/mc_comm_determinism.c b/src/mc/mc_comm_determinism.c
index 1ac3784..9c01b85 100644 (file)
--- a/src/mc/mc_comm_determinism.c
+++ b/src/mc/mc_comm_determinism.c
@@ -4,6 +4,10 @@
 /* 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 "mc_state.h"
+#include "mc_comm_pattern.h"
+#include "mc_request.h"
+#include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
 

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index 0958d2d..4745d3a 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -9,6 +9,9 @@
 #include <boost/unordered_set.hpp>
 
 #include "internal_config.h"
+#include "mc_object_info.h"
+#include "mc_safety.h"
+#include "mc_liveness.h"
 #include "mc_private.h"
 
 #ifdef HAVE_SMPI

diff --git a/src/mc/mc_config.c b/src/mc/mc_config.c
index 1f0d836..07c9179 100644 (file)
--- a/src/mc/mc_config.c
+++ b/src/mc/mc_config.c
@@ -14,6 +14,7 @@
 #include <simgrid/sg_config.h>
 
 #ifdef HAVE_MC
+#include "mc_safety.h"
 #include "mc_private.h"
 #endif
 

diff --git a/src/mc/mc_diff.c b/src/mc/mc_diff.c
index a9b8dd4..03dfb36 100644 (file)
--- a/src/mc/mc_diff.c
+++ b/src/mc/mc_diff.c
@@ -10,8 +10,10 @@
 #include "xbt/str.h"
 #include "mc/mc.h"
 #include "xbt/mmalloc.h"
+#include "mc_object_info.h"
 #include "mc/datatypes.h"
 #include "mc/mc_private.h"
+#include "mc/mc_snapshot.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
                                 "Logging specific to mc_diff in mc");

diff --git a/src/mc/mc_dwarf.c b/src/mc/mc_dwarf.c
index 40046c2..2b2c2a0 100644 (file)
--- a/src/mc/mc_dwarf.c
+++ b/src/mc/mc_dwarf.c
@@ -14,6 +14,7 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
+#include "mc_object_info.h"
 #include "mc_private.h"
 
 static void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable);

diff --git a/src/mc/mc_dwarf_expression.c b/src/mc/mc_dwarf_expression.c
index ea58470..7653210 100644 (file)
--- a/src/mc/mc_dwarf_expression.c
+++ b/src/mc/mc_dwarf_expression.c
@@ -10,6 +10,8 @@
 #include <dwarf.h>
 #include <elfutils/libdw.h>
 
+#include "mc_object_info.h"
+#include "mc_snapshot.h"
 #include "mc_private.h"
 
 static int mc_dwarf_push_value(mc_expression_state_t state, Dwarf_Off value)

diff --git a/src/mc/mc_forward.h b/src/mc/mc_forward.h
index dd74458..58fde4c 100644 (file)
--- a/src/mc/mc_forward.h
+++ b/src/mc/mc_forward.h
@@ -16,4 +16,10 @@ typedef struct s_memory_map s_memory_map_t, *memory_map_t;
 typedef struct s_dw_variable s_dw_variable_t, *dw_variable_t;
 typedef struct s_dw_frame s_dw_frame_t, *dw_frame_t;
 
+typedef struct s_mc_pages_store s_mc_pages_store_t, *mc_pages_store_t;
+typedef struct s_mc_snapshot s_mc_snapshot_t, *mc_snapshot_t;
+
+typedef struct s_mc_model_checker s_mc_model_checker_t, *mc_model_checker_t;
+extern mc_model_checker_t mc_model_checker;
+
 #endif

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index ec5e3c3..00b8f2b 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -23,6 +23,13 @@
 
 #ifdef HAVE_MC
 #include "../xbt/mmalloc/mmprivate.h"
+#include "mc_object_info.h"
+#include "mc_comm_pattern.h"
+#include "mc_request.h"
+#include "mc_safety.h"
+#include "mc_memory_map.h"
+#include "mc_snapshot.h"
+#include "mc_liveness.h"
 #include "mc_private.h"
 #endif
 #include "mc_record.h"

diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c
index 1f6dd21..13cab5e 100644 (file)
--- a/src/mc/mc_ignore.c
+++ b/src/mc/mc_ignore.c
@@ -5,8 +5,10 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "internal_config.h"
+#include "mc_object_info.h"
 #include "mc_private.h"
 #include "smpi/private.h"
+#include "mc/mc_snapshot.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
                                 "Logging specific to MC ignore mechanism");

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 841b102..1b8c3dd 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -4,11 +4,17 @@
 /* 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 "mc_private.h"
-#include "mc_record.h"
 #include <unistd.h>
 #include <sys/wait.h>
 
+#include <xbt/dynar.h>
+#include <xbt/automaton.h>
+
+#include "mc_request.h"
+#include "mc_liveness.h"
+#include "mc_private.h"
+#include "mc_record.h"
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 

diff --git a/src/mc/mc_location.h b/src/mc/mc_location.h
index 2929200..45657f4 100644 (file)
--- a/src/mc/mc_location.h
+++ b/src/mc/mc_location.h
@@ -15,6 +15,8 @@
 #include <elfutils/libdw.h>
 
 #include <simgrid_config.h>
+#include "mc_interface.h"
+#include "mc_object_info.h"
 #include "mc_forward.h"
 
 SG_BEGIN_DECL()

diff --git a/src/mc/mc_member.c b/src/mc/mc_member.c
index ff7667d..b5ee069 100644 (file)
--- a/src/mc/mc_member.c
+++ b/src/mc/mc_member.c
@@ -4,6 +4,7 @@
 /* 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 "mc_object_info.h"
 #include "mc_private.h"
 
 /** Resolve snapshot in the process address space
@@ -38,4 +39,3 @@ void *mc_member_resolve(const void *base, dw_type_t type, dw_type_t member,
   else
     return (void *) state.stack[state.stack_size - 1];
 }
-

diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c
index 655418d..b474b0c 100644 (file)
--- a/src/mc/mc_memory.c
+++ b/src/mc/mc_memory.c
@@ -6,9 +6,12 @@
 
 #include <sys/stat.h>
 #include <fcntl.h>
+
+#include "xbt/log.h"
+
 #include "mc/mc.h"
+#include "mc_object_info.h"
 #include "mc_private.h"
-#include "xbt/log.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory, mc,
                                 "Logging specific to MC (memory)");

diff --git a/src/mc/mc_memory_map.h b/src/mc/mc_memory_map.h
index 6d118d0..afa2b58 100644 (file)
--- a/src/mc/mc_memory_map.h
+++ b/src/mc/mc_memory_map.h
@@ -8,6 +8,7 @@
 #define MC_MEMORY_MAP_H
 
 #include <simgrid_config.h>
+#include "mc_forward.h"
 
 SG_BEGIN_DECL()
 

diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h
index 74df0d7..9ab2813 100644 (file)
--- a/src/mc/mc_model_checker.h
+++ b/src/mc/mc_model_checker.h
@@ -3,11 +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. */
+ 
+#ifndef MC_MODEL_CHECKER_H
+#define MC_MODEL_CHECKER_H
 
 #include <simgrid_config.h>
 
-#ifndef MC_MODEL_CHECKER_H
-#define MC_MODEL_CHECKER_H
+#include "mc_forward.h"
 
 SG_BEGIN_DECL()
 
@@ -18,18 +20,17 @@ SG_BEGIN_DECL()
  *  By moving as much state as possible in this structure allocated
  *  on the model-chercker heap, we avoid those issues.
  */
-typedef struct s_mc_model_checker {
+struct s_mc_model_checker {
   // This is the parent snapshot of the current state:
   mc_snapshot_t parent_snapshot;
   mc_pages_store_t pages;
   int fd_clear_refs;
   int fd_pagemap;
   xbt_dynar_t record;
-} s_mc_model_checker_t, *mc_model_checker_t;
+};
 
 mc_model_checker_t MC_model_checker_new(void);
 void MC_model_checker_delete(mc_model_checker_t mc);
-extern mc_model_checker_t mc_model_checker;
 
 SG_END_DECL()
 

diff --git a/src/mc/mc_page_snapshot.cpp b/src/mc/mc_page_snapshot.cpp
index a231848..499e5f2 100644 (file)
--- a/src/mc/mc_page_snapshot.cpp
+++ b/src/mc/mc_page_snapshot.cpp
@@ -1,6 +1,7 @@
 #include "mc_page_store.h"
 #include "mc_mmu.h"
 #include "mc_private.h"
+#include "mc_snapshot.h"
 
 #include <xbt/mmalloc.h>
 

diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c
index 29910e6..62e1f38 100644 (file)
--- a/src/mc/mc_pair.c
+++ b/src/mc/mc_pair.c
@@ -4,6 +4,8 @@
 /* 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 <xbt.h>
+#include "mc_liveness.h"
 #include "mc_private.h"
 
 mc_pair_t MC_pair_new()

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index b0f4fc6..1ef0f8d 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -9,6 +9,7 @@
 
 #include "simgrid_config.h"
 #include <stdio.h>
+#include <stdint.h>
 #include <stdbool.h>
 #ifndef WIN32
 #include <sys/mman.h>
@@ -32,20 +33,6 @@
 #include "xbt/parmap.h"
 
 #include "mc_forward.h"
-#include "mc_mmu.h"
-#include "mc_page_store.h"
-#include "mc_interface.h"
-#include "mc_mmalloc.h"
-#include "mc_model_checker.h"
-#include "mc_snapshot.h"
-#include "mc_object_info.h"
-#include "mc_location.h"
-#include "mc_state.h"
-#include "mc_comm_pattern.h"
-#include "mc_request.h"
-#include "mc_safety.h"
-#include "mc_liveness.h"
-#include "mc_memory_map.h"
 
 SG_BEGIN_DECL()
 

diff --git a/src/mc/mc_record.c b/src/mc/mc_record.c
index b898e56..d9d79e1 100644 (file)
--- a/src/mc/mc_record.c
+++ b/src/mc/mc_record.c
@@ -10,11 +10,13 @@
 #include <xbt.h>
 #include <simgrid/simix.h>
 
-#include "mc_base.h"
 #include "mc_record.h"
+#include "mc_base.h"
 
 #ifdef HAVE_MC
 #include "mc_private.h"
+#include "mc_model_checker.h"
+#include "mc_state.h"
 #endif
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_record, mc,

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 234c5d2..af7f1ef 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -4,6 +4,8 @@
 /* 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 "mc_request.h"
+#include "mc_safety.h"
 #include "mc_private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 401c43b..658c185 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -4,6 +4,9 @@
 /* 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 "mc_state.h"
+#include "mc_request.h"
+#include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
 

diff --git a/src/mc/mc_snapshot.c b/src/mc/mc_snapshot.c
index bc1b553..97c4017 100644 (file)
--- a/src/mc/mc_snapshot.c
+++ b/src/mc/mc_snapshot.c
@@ -9,6 +9,7 @@
 #include "internal_config.h"
 #include "smpi/private.h"
 
+#include "mc_snapshot.h"
 #include "mc_private.h"
 #include "mc_mmu.h"
 #include "mc_page_store.h"
@@ -172,6 +173,8 @@ int mc_snapshot_memcmp(
 #include <sys/mman.h>
 
 #include "mc/mc_private.h"
+#include "mc/mc_snapshot.h"
+#include "mc/mc_mmu.h"
 
 XBT_TEST_SUITE("mc_snapshot", "Snapshots");
 
@@ -281,4 +284,3 @@ static void test_snapshot(bool sparse_checkpoint) {
 }
 
 #endif /* SIMGRID_TEST */
-

diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h
index 0f46848..352ae8b 100644 (file)
--- a/src/mc/mc_snapshot.h
+++ b/src/mc/mc_snapshot.h
@@ -3,22 +3,23 @@
 
 /* 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 MC_SNAPSHOT_H
+#define MC_SNAPSHOT_H
+
 #include <sys/types.h> // off_t
 #include <stdint.h> // size_t
 
+#include <simgrid_config.h>
+#include "../xbt/mmalloc/mmprivate.h"
 #include <xbt/asserts.h>
 #include <xbt/dynar.h>
-#include <simgrid_config.h>
 
 #include "mc_forward.h"
-#include "mc_page_store.h"
 #include "mc_model_checker.h"
+#include "mc_page_store.h"
 #include "mc_mmalloc.h"
 
-#ifndef MC_SNAPSHOT_H
-#define MC_SNAPSHOT_H
-
 SG_BEGIN_DECL()
 
 void mc_softdirty_reset();
@@ -150,7 +151,7 @@ typedef struct s_fd_infos{
   int flags;
 }s_fd_infos_t, *fd_infos_t;
 
-typedef struct s_mc_snapshot{
+struct s_mc_snapshot{
   size_t heap_bytes_used;
   mc_mem_region_t regions[NB_REGIONS];
   xbt_dynar_t enabled_processes;
@@ -163,7 +164,7 @@ typedef struct s_mc_snapshot{
   xbt_dynar_t ignored_data;
   int total_fd;
   fd_infos_t *current_fd;
-} s_mc_snapshot_t;
+};
 
 /** @brief Process index used when no process is available
  *

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index 4724523..e9b4b04 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -6,6 +6,8 @@
 
 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
+#include "mc_state.h"
+#include "mc_request.h"
 #include "mc_private.h"
 
 /**

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index e5927ec..1bc0316 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -9,6 +9,7 @@
 
 #include <simgrid_config.h>
 #include "../simix/smx_private.h"
+#include "mc_snapshot.h"
 
 SG_BEGIN_DECL()
 

diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c
index ac7c56b..8ac5d0f 100644 (file)
--- a/src/mc/mc_visited.c
+++ b/src/mc/mc_visited.c
@@ -4,10 +4,14 @@
 /* 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 "mc_private.h"
 #include <unistd.h>
 #include <sys/wait.h>
 
+#include "mc_comm_pattern.h"
+#include "mc_safety.h"
+#include "mc_liveness.h"
+#include "mc_private.h"
+
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
                                 "Logging specific to state equaity detection mechanisms");
 

diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c
index e63cab7..b867a86 100644 (file)
--- a/src/mc/memory_map.c
+++ b/src/mc/memory_map.c
@@ -4,6 +4,7 @@
 /* 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 "mc_memory_map.h"
 #include "mc_private.h"
 #include <stdlib.h>
 

diff --git a/src/simix/popping_generated.c b/src/simix/popping_generated.c
index 0a68930..b339a4a 100644 (file)
--- a/src/simix/popping_generated.c
+++ b/src/simix/popping_generated.c
@@ -15,7 +15,6 @@
 
 #include "smx_private.h"
 #ifdef HAVE_MC
-#include "mc/mc_private.h"
 #endif
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);

diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py
index 99a968a..41bd69d 100755 (executable)
--- a/src/simix/simcalls.py
+++ b/src/simix/simcalls.py
@@ -281,7 +281,7 @@ if __name__=='__main__':
   
   fd.write('#include "smx_private.h"\n');
   fd.write('#ifdef HAVE_MC\n');
-  fd.write('#include "mc/mc_private.h"\n');
+  # fd.write('#include "mc/mc_private.h"\n');
   fd.write('#endif\n');
   fd.write('\n');
   fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n');

diff --git a/teshsuite/mc/dwarf/dwarf.c b/teshsuite/mc/dwarf/dwarf.c
index 7378579..8b22d4b 100644 (file)
--- a/teshsuite/mc/dwarf/dwarf.c
+++ b/teshsuite/mc/dwarf/dwarf.c
@@ -15,6 +15,7 @@
 #include <mc/mc.h>
 
 #include "../../src/include/mc/datatypes.h"
+#include "../../src/mc/mc_object_info.h"
 #include "../../src/mc/mc_private.h"
 
 int test_some_array[4][5][6];

diff --git a/teshsuite/mc/dwarf_expression/dwarf_expression.c b/teshsuite/mc/dwarf_expression/dwarf_expression.c
index 905f88a..998b779 100644 (file)
--- a/teshsuite/mc/dwarf_expression/dwarf_expression.c
+++ b/teshsuite/mc/dwarf_expression/dwarf_expression.c
@@ -13,6 +13,7 @@
 #include <stdlib.h>
 
 #include "../src/mc/mc_private.h"
+#include "../src/mc/mc_object_info.h"
 
 static
 uintptr_t eval_binary_operation(mc_expression_state_t state, int op, uintptr_t a, uintptr_t b) {