#include "xbt/dynar.h"
#include "xbt/dict.h"
-#include "src/mc/mc_forward.h"
SG_BEGIN_DECL()
#include <xbt/base.h>
#include <xbt/range.hpp>
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "src/mc/LocationList.hpp"
#include "src/mc/Variable.hpp"
#include "src/mc/Frame.hpp"
PageStore page_store_;
std::unique_ptr<Process> process_;
public:
- mc_snapshot_t parent_snapshot_;
+ simgrid::mc::Snapshot* parent_snapshot_;
public:
ModelChecker(ModelChecker const&) = delete;
#include <xbt/base.h>
#include "src/xbt/memory_map.hpp"
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "src/mc/Type.hpp"
#include "src/mc/Frame.hpp"
#include <dwarf.h>
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "src/mc/LocationList.hpp"
namespace simgrid {
#include <string>
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "src/mc/LocationList.hpp"
namespace simgrid {
#endif
static
-void add_region(int index, mc_snapshot_t snapshot,
+void add_region(int index, simgrid::mc::Snapshot* snapshot,
simgrid::mc::RegionType type,
simgrid::mc::ObjectInformation* object_info,
void *start_addr, void* permanent_addr,
return;
}
-static void get_memory_regions(simgrid::mc::Process* process, mc_snapshot_t snapshot)
+static void get_memory_regions(simgrid::mc::Process* process, simgrid::mc::Snapshot* snapshot)
{
const size_t n = process->object_infos.size();
snapshot->snapshot_regions.resize(n + 1);
return std::move(result);
};
-static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(mc_snapshot_t * snapshot)
+static std::vector<s_mc_snapshot_stack_t> take_snapshot_stacks(simgrid::mc::Snapshot* * snapshot)
{
std::vector<s_mc_snapshot_stack_t> res;
}
-static void snapshot_handle_ignore(mc_snapshot_t snapshot)
+static void snapshot_handle_ignore(simgrid::mc::Snapshot* snapshot)
{
xbt_assert(snapshot->process());
}
-static void snapshot_ignore_restore(mc_snapshot_t snapshot)
+static void snapshot_ignore_restore(simgrid::mc::Snapshot* snapshot)
{
for (auto const& ignored_data : snapshot->ignored_data)
snapshot->process()->write_bytes(
return std::move(fds);
}
-mc_snapshot_t take_snapshot(int num_state)
+simgrid::mc::Snapshot* take_snapshot(int num_state)
{
XBT_DEBUG("Taking snapshot %i", num_state);
simgrid::mc::Process* mc_process = &mc_model_checker->process();
- mc_snapshot_t snapshot = new simgrid::mc::Snapshot(mc_process);
+ simgrid::mc::Snapshot* snapshot = new simgrid::mc::Snapshot(mc_process);
snapshot->num_state = num_state;
}
static inline
-void restore_snapshot_regions(mc_snapshot_t snapshot)
+void restore_snapshot_regions(simgrid::mc::Snapshot* snapshot)
{
for(std::unique_ptr<s_mc_mem_region_t> const& region : snapshot->snapshot_regions) {
// For privatized, variables we decided it was not necessary to take the snapshot:
}
static inline
-void restore_snapshot_fds(mc_snapshot_t snapshot)
+void restore_snapshot_fds(simgrid::mc::Snapshot* snapshot)
{
if (mc_mode == MC_MODE_SERVER)
xbt_die("FD snapshot not implemented in client/server mode.");
}
}
-void restore_snapshot(mc_snapshot_t snapshot)
+void restore_snapshot(simgrid::mc::Snapshot* snapshot)
{
XBT_DEBUG("Restore snapshot %i", snapshot->num_state);
const bool use_soft_dirty = _sg_mc_sparse_checkpoint && _sg_mc_soft_dirty;
#include <xbt/sysdep.h>
#include "src/internal_config.h"
+#include "src/mc/mc_forward.hpp"
#include "src/mc/mc_safety.h"
#include "src/mc/mc_liveness.h"
#include "src/mc/mc_private.h"
static int compare_areas_with_type(ComparisonState& state,
int process_index,
- void* real_area1, mc_snapshot_t snapshot1, mc_mem_region_t region1,
- void* real_area2, mc_snapshot_t snapshot2, mc_mem_region_t region2,
+ void* real_area1, simgrid::mc::Snapshot* snapshot1, mc_mem_region_t region1,
+ void* real_area2, simgrid::mc::Snapshot* snapshot2, mc_mem_region_t region2,
simgrid::mc::Type* type, int pointer_level)
{
simgrid::mc::Process* process = &mc_model_checker->process();
static int compare_global_variables(simgrid::mc::ObjectInformation* object_info,
int process_index,
mc_mem_region_t r1,
- mc_mem_region_t r2, mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2)
+ mc_mem_region_t r2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2)
{
xbt_assert(r1 && r2, "Missing region.");
}
static int compare_local_variables(int process_index,
- mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2,
+ simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2,
mc_snapshot_stack_t stack1,
mc_snapshot_stack_t stack2)
{
{
simgrid::mc::Process* process = &mc_model_checker->process();
- mc_snapshot_t s1, s2;
+ simgrid::mc::Snapshot* s1;
+ simgrid::mc::Snapshot* s2;
int num1, num2;
if (_sg_mc_liveness) { /* Liveness MC */
// TODO, have a robust way to find it in O(1)
static inline
-mc_mem_region_t MC_get_heap_region(mc_snapshot_t snapshot)
+mc_mem_region_t MC_get_heap_region(simgrid::mc::Snapshot* snapshot)
{
size_t n = snapshot->snapshot_regions.size();
for (size_t i=0; i!=n; ++i) {
xbt_die("No heap region");
}
-int mmalloc_compare_heap(mc_snapshot_t snapshot1, mc_snapshot_t snapshot2)
+int mmalloc_compare_heap(simgrid::mc::Snapshot* snapshot1, simgrid::mc::Snapshot* snapshot2)
{
simgrid::mc::Process* process = &mc_model_checker->process();
struct s_mc_diff *state = mc_diff_info;
*/
static int compare_heap_area_without_type(struct s_mc_diff *state, int process_index,
const void *real_area1, const void *real_area2,
- mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2,
+ simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2,
xbt_dynar_t previous, int size,
int check_ignore)
{
*/
static int compare_heap_area_with_type(struct s_mc_diff *state, int process_index,
const void *real_area1, const void *real_area2,
- mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2,
+ simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2,
xbt_dynar_t previous, simgrid::mc::Type* type,
int area_size, int check_ignore,
int pointer_level)
*/
static simgrid::mc::Type* get_offset_type(void *real_base_address, simgrid::mc::Type* type,
int offset, int area_size,
- mc_snapshot_t snapshot, int process_index)
+ simgrid::mc::Snapshot* snapshot, int process_index)
{
// Beginning of the block, the infered variable type if the type of the block:
* @param pointer_level
* @return 0 (same), 1 (different), -1
*/
-int compare_heap_area(int process_index, const void *area1, const void *area2, mc_snapshot_t snapshot1,
- mc_snapshot_t snapshot2, xbt_dynar_t previous,
+int compare_heap_area(int process_index, const void *area1, const void *area2, simgrid::mc::Snapshot* snapshot1,
+ simgrid::mc::Snapshot* snapshot2, xbt_dynar_t previous,
simgrid::mc::Type* type, int pointer_level)
{
simgrid::mc::Process* process = &mc_model_checker->process();
+++ /dev/null
-/* Copyright (c) 2007-2015. 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. */
-
-/** \file mc_forward.h
- *
- * Define type names for pointers of MC objects for the C code
- */
-
-#ifndef SIMGRID_MC_FORWARD_H
-#define SIMGRID_MC_FORWARD_H
-
-#ifdef __cplusplus
-
-// If we're in C++, we give the real definition:
-#include "mc_forward.hpp"
-typedef simgrid::mc::Snapshot *mc_snapshot_t;
-typedef simgrid::mc::Type *mc_type_t;
-
-#else
-
-// Otherwise we use dummy opaque structs:
-typedef struct _mc_snapshot_t *mc_snapshot_t;
-typedef struct _s_mc_type_t *mc_type_t;
-
-#endif
-
-#endif
#include "xbt/parmap.h"
#include <xbt/base.h>
-#include "src/mc/mc_forward.h"
+#ifdef __cplusplus
+#include "src/mc/mc_forward.hpp"
+#endif
+
#include "src/mc/mc_protocol.h"
SG_BEGIN_DECL()
int modelcheck_safety(void);
struct XBT_PRIVATE VisitedState {
- mc_snapshot_t system_state;
+ simgrid::mc::Snapshot* system_state;
size_t heap_bytes_used;
int nb_processes;
int num;
* @return same as memcmp
* */
int MC_snapshot_memcmp(
- const void* addr1, mc_snapshot_t snapshot1,
- const void* addr2, mc_snapshot_t snapshot2, int process_index, size_t size)
+ const void* addr1, simgrid::mc::Snapshot* snapshot1,
+ const void* addr2, simgrid::mc::Snapshot* snapshot2, int process_index, size_t size)
{
mc_mem_region_t region1 = mc_get_snapshot_region(addr1, snapshot1, process_index);
mc_mem_region_t region2 = mc_get_snapshot_region(addr2, snapshot2, process_index);
} s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
typedef struct s_mc_global_t {
- mc_snapshot_t snapshot;
+ simgrid::mc::Snapshot* snapshot;
int prev_pair;
char *prev_req;
int initial_communications_pattern_done;
extern "C" {
static inline __attribute__ ((always_inline))
-mc_mem_region_t mc_get_region_hinted(void* addr, mc_snapshot_t snapshot, int process_index, mc_mem_region_t region)
+mc_mem_region_t mc_get_region_hinted(void* addr, simgrid::mc::Snapshot* snapshot, int process_index, mc_mem_region_t region)
{
if (region->contain(simgrid::mc::remote(addr)))
return region;
return mc_get_snapshot_region(addr, snapshot, process_index);
}
-static const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
+static const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot);
}
namespace simgrid {
namespace mc {
-XBT_PRIVATE mc_snapshot_t take_snapshot(int num_state);
-XBT_PRIVATE void restore_snapshot(mc_snapshot_t);
+XBT_PRIVATE simgrid::mc::Snapshot* take_snapshot(int num_state);
+XBT_PRIVATE void restore_snapshot(simgrid::mc::Snapshot*);
}
}
const void* addr1, mc_mem_region_t region1,
const void* addr2, mc_mem_region_t region2, std::size_t size);
XBT_PRIVATE int MC_snapshot_memcmp(
- const void* addr1, mc_snapshot_t snapshot1,
- const void* addr2, mc_snapshot_t snapshot2, int process_index, std::size_t size);
+ const void* addr1, simgrid::mc::Snapshot* snapshot1,
+ const void* addr2, simgrid::mc::Snapshot* snapshot2, int process_index, std::size_t size);
static inline __attribute__ ((always_inline))
-const void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot)
+const void* mc_snapshot_get_heap_end(simgrid::mc::Snapshot* snapshot)
{
if(snapshot==NULL)
xbt_die("snapshot is NULL");
s_smx_simcall_t executed_req; /* The executed request of the state */
int req_num; /* The request number (in the case of a
multi-request like waitany ) */
- mc_snapshot_t system_state; /* Snapshot of system state */
+ simgrid::mc::Snapshot* system_state; /* Snapshot of system state */
int num;
int in_visited_states;
// comm determinism verification (xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>):
#include "src/mc/mc_replay.h"
#include "smx_private.h"
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "xbt/ex.h"
#include "mc/mc.h"
#include "src/simix/smx_host_private.h"
*/
#include "smx_private.h"
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#include "xbt/ex.h"
#include <simgrid/simix.hpp>
#include <xbt/base.h>
#include "smx_private.h"
#if HAVE_MC
-#include "src/mc/mc_forward.h"
+#include "src/mc/mc_forward.hpp"
#endif
XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);
XBT_PUBLIC_DATA(const char*) simcall_names[]; /* Name of each simcall */
#include "popping_enum.h" /* Definition of e_smx_simcall_t, with one value per simcall */
-#include "src/mc/mc_forward.h" /* Definition of mc_snapshot_t, used by one simcall */
typedef int (*simix_match_func_t)(void *, void *, smx_synchro_t);
typedef void (*simix_copy_data_func_t)(smx_synchro_t, void*, size_t);
fd.write('#include <xbt/base.h>\n')
fd.write('#include "smx_private.h"\n')
fd.write('#if HAVE_MC\n')
- fd.write('#include "src/mc/mc_forward.h"\n')
+ fd.write('#include "src/mc/mc_forward.hpp"\n')
fd.write('#endif\n')
fd.write('\n')
fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n')
#
fd = header('popping_bodies.cpp')
fd.write('#include "smx_private.h"\n')
- fd.write('#include "src/mc/mc_forward.h"\n')
+ fd.write('#include "src/mc/mc_forward.hpp"\n')
fd.write('#include "xbt/ex.h"\n')
fd.write('#include <simgrid/simix.hpp>\n')
handle(fd, Simcall.body, simcalls, simcalls_dict)
src/mc/Type.hpp
src/mc/Variable.cpp
src/mc/Variable.hpp
-
- src/mc/mc_forward.h
src/mc/mc_forward.hpp
src/mc/Process.hpp
src/mc/Process.cpp