#include <dirent.h>
#include "internal_config.h"
+#include "mc_memory_map.h"
#include "mc_private.h"
#include "xbt/module.h"
#include <xbt/mmalloc.h>
#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,
/* 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"
#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
#include <simgrid/sg_config.h>
#ifdef HAVE_MC
+#include "mc_safety.h"
#include "mc_private.h"
#endif
#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");
#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);
#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)
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
#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"
* 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");
/* 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");
#include <elfutils/libdw.h>
#include <simgrid_config.h>
+#include "mc_interface.h"
+#include "mc_object_info.h"
#include "mc_forward.h"
SG_BEGIN_DECL()
/* 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
else
return (void *) state.stack[state.stack_size - 1];
}
-
#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)");
#define MC_MEMORY_MAP_H
#include <simgrid_config.h>
+#include "mc_forward.h"
SG_BEGIN_DECL()
/* 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()
* 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()
#include "mc_page_store.h"
#include "mc_mmu.h"
#include "mc_private.h"
+#include "mc_snapshot.h"
#include <xbt/mmalloc.h>
/* 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()
#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()
#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,
/* 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,
/* 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"
#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"
#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");
}
#endif /* SIMGRID_TEST */
-
/* 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();
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;
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
*
#include "../simix/smx_private.h"
#include "xbt/fifo.h"
+#include "mc_state.h"
+#include "mc_request.h"
#include "mc_private.h"
/**
#include <simgrid_config.h>
#include "../simix/smx_private.h"
+#include "mc_snapshot.h"
SG_BEGIN_DECL()
/* 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");
/* 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>
#include "smx_private.h"
#ifdef HAVE_MC
-#include "mc/mc_private.h"
#endif
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
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');
#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];
#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) {