Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove useless header #includes
authorGabriel Corona <gabriel.corona@loria.fr>
Tue, 2 Dec 2014 13:02:26 +0000 (14:02 +0100)
committerGabriel Corona <gabriel.corona@loria.fr>
Thu, 4 Dec 2014 09:37:31 +0000 (10:37 +0100)
32 files changed:
src/mc/mc_checkpoint.c
src/mc/mc_comm_determinism.c
src/mc/mc_compare.cpp
src/mc/mc_config.c
src/mc/mc_diff.c
src/mc/mc_dwarf.c
src/mc/mc_dwarf_expression.c
src/mc/mc_forward.h
src/mc/mc_global.c
src/mc/mc_ignore.c
src/mc/mc_liveness.c
src/mc/mc_location.h
src/mc/mc_member.c
src/mc/mc_memory.c
src/mc/mc_memory_map.h
src/mc/mc_model_checker.h
src/mc/mc_page_snapshot.cpp
src/mc/mc_pair.c
src/mc/mc_private.h
src/mc/mc_record.c
src/mc/mc_request.c
src/mc/mc_safety.c
src/mc/mc_snapshot.c
src/mc/mc_snapshot.h
src/mc/mc_state.c
src/mc/mc_state.h
src/mc/mc_visited.c
src/mc/memory_map.c
src/simix/popping_generated.c
src/simix/simcalls.py
teshsuite/mc/dwarf/dwarf.c
teshsuite/mc/dwarf_expression/dwarf_expression.c

index d20592646aa4b3e7adba265024eb2ed137e99163..8680749e64830a13e11b0a0a95505dfe2a193792 100644 (file)
@@ -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,
index 1ac378464248c6470cbbf8e550f5ec4df0fa748e..9c01b85e0e32afc04d9fb9cd1a59b22da01b55cc 100644 (file)
@@ -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"
 
index 0958d2d995fb57c16a7cd3fce1c011c234406fb7..4745d3a4eee42df64e9b0fa8eca57ac14f7aaf32 100644 (file)
@@ -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
index 1f0d83688387bad8dfae454d7365190720ebbdf0..07c917988903a88a735087e9a976ec796e801157 100644 (file)
@@ -14,6 +14,7 @@
 #include <simgrid/sg_config.h>
 
 #ifdef HAVE_MC
+#include "mc_safety.h"
 #include "mc_private.h"
 #endif
 
index a9b8dd40b773cd2501234d855e08ade9b793d6e0..03dfb36abacdfbdc36df0564dbb9e9472dbd1452 100644 (file)
 #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");
index 40046c2340ff5f13cc833099e1c2d4ad43131237..2b2c2a0aaa93ea414ed54eb5eba7fd38a379ae24 100644 (file)
@@ -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);
index ea58470370529f01790338228c42fd162d391dea..7653210fafff442703e3aecbb16117f4026d2e35 100644 (file)
@@ -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)
index dd744585383521736f080693d4177356ace4d5c5..58fde4cbdedffa9ab81ce2b15ac68945621c12da 100644 (file)
@@ -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
index ec5e3c301ef0f118c68b00a710e09775136180c4..00b8f2b39fbf9fd1a6f55021c6ee61fa3e6ea371 100644 (file)
 
 #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"
index 1f6dd21cee7f74984fa2aecf5eee4895db8adcc4..13cab5e2e2e569d39333120c3ba1d33fcffde6d3 100644 (file)
@@ -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");
index 841b1026890415a614328f591ad26571b3a91e38..1b8c3dd1633488f7efcab842577b75c1e9adfb64 100644 (file)
@@ -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");
 
index 29292006d525535e9ef9a80c71a7660fb121cb69..45657f4551cad7a8f4755c8b092932c7455a8565 100644 (file)
@@ -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()
index ff7667d8a70e48609839e6c85f9685eb3c380984..b5ee0690f07791015b80e32b146d7f620a26b900 100644 (file)
@@ -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];
 }
-
index 655418da53a9960b1235b34b362b9b79a40e0bff..b474b0ced65abf4668042c170138c878cb726c88 100644 (file)
@@ -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)");
index 6d118d001382cbdb8ee11015b01079059fa82c56..afa2b58c672b80f012c29f388044f97ce0c5cc46 100644 (file)
@@ -8,6 +8,7 @@
 #define MC_MEMORY_MAP_H
 
 #include <simgrid_config.h>
+#include "mc_forward.h"
 
 SG_BEGIN_DECL()
 
index 74df0d7cecfe3d0b58af155bd6d7867e0dc8df36..9ab2813c23976732e69cdf0b3a76575af4dae4cc 100644 (file)
@@ -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()
 
index a231848005326bebaa20169d6ba10c120cc7be8c..499e5f210fa876b7192db6225343e1c7fc419389 100644 (file)
@@ -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>
 
index 29910e6cff723d49f8298435c3c455b582c1c4e7..62e1f385e8f55b2aa44c2a816317005ac2440e29 100644 (file)
@@ -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()
index b0f4fc6df35a1a520d0d8243d2606c24cec9b525..1ef0f8d05ba40cfd961b8b11d46735d4b11efb2d 100644 (file)
@@ -9,6 +9,7 @@
 
 #include "simgrid_config.h"
 #include <stdio.h>
+#include <stdint.h>
 #include <stdbool.h>
 #ifndef WIN32
 #include <sys/mman.h>
 #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()
 
index b898e566d700ac9d80c952752eb74a24f2b05955..d9d79e1de8fa9f3f66f503c8fe1475c7988d6777 100644 (file)
 #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,
index 234c5d27d3cef073a363d43ba9775ebd5fee6207..af7f1ef76604adb2f9d760040542bb196d32153f 100644 (file)
@@ -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,
index 401c43b772509283ff94e75049afbd8ee4593eaa..658c18582f3c9a21d4c4516182dd67d1ac05007f 100644 (file)
@@ -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"
 
index bc1b5535d1949d134305dabb788c4f18d144da98..97c4017b0ec0bfb4506c93d1447fcbc917d8b609 100644 (file)
@@ -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 */
-
index 0f46848c677fd8e904f3020f42088663a25a6eee..352ae8bcfc31473c97d6917167b39dc8f0ecbd56 100644 (file)
@@ -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
  *
index 47245230c2aaad3804539750501cf0cf0b888507..e9b4b0449001e4018206c6bd4f6e5f0c0b855ed7 100644 (file)
@@ -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"
 
 /**
index e5927ecc82aa52705df8673739dd8eaf11b1fc59..1bc0316dd9ef7b1c0d2dd753784971693805d88a 100644 (file)
@@ -9,6 +9,7 @@
 
 #include <simgrid_config.h>
 #include "../simix/smx_private.h"
+#include "mc_snapshot.h"
 
 SG_BEGIN_DECL()
 
index ac7c56b3c421075458162148d98bd84526b43bf8..8ac5d0fa73d6fea287a20a84d6d0333fed2a0e86 100644 (file)
@@ -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");
 
index e63cab775fdf8ebc8a854671c146d43acdfa4ce1..b867a86d6ffd2e405b571b67aacbe22a6b9428ba 100644 (file)
@@ -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>
 
index 0a6893003f9a6d97fd9107497d3a7db1816ffade..b339a4a1a05a9322184d2fdbaec040521f45899d 100644 (file)
@@ -15,7 +15,6 @@
 
 #include "smx_private.h"
 #ifdef HAVE_MC
-#include "mc/mc_private.h"
 #endif
 
 XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
index 99a968af3fb47371b735a83ccaf6b2dbb7d507b7..41bd69d13a45e7be4a6de69bae7176e009186e81 100755 (executable)
@@ -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');
index 7378579efdc8781a17b8f32e22899bd5bc96e626..8b22d4be317e0164c0d5e95d79e03af8be4f7cd2 100644 (file)
@@ -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];
index 905f88aee8d648f0215045aa24b3a28b0d68d32c..998b779aa1f31395eab39a9d26b6bce4e9be2dbc 100644 (file)
@@ -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) {