void MC_restore_snapshot(mc_snapshot_t);
void MC_free_snapshot(mc_snapshot_t);
+
/********************************* MC Global **********************************/
extern double *mc_time;
};
#define MC_SET_RAW_MEM mmalloc_set_current_heap(raw_heap)
-#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+#define MC_UNSET_RAW_MEM mmalloc_set_current_heap(std_heap)
+
+extern int raw_mem_set;
/******************************* MEMORY MAPPINGS ***************************/
/* These functions and data structures implements a binary interface for */
/********************************** DPOR for safety **************************************/
+typedef enum {
+ e_mc_reduce_unset,
+ e_mc_reduce_none,
+ e_mc_reduce_dpor
+} e_mc_reduce_t;
+extern e_mc_reduce_t mc_reduce_kind;
void MC_dpor_init(void);
void MC_dpor(void);
/********************************** Double-DFS for liveness property**************************************/
extern mc_snapshot_t initial_snapshot_liveness;
-extern xbt_automaton_t automaton;
+extern xbt_automaton_t _mc_property_automaton;
typedef struct s_mc_pair{
mc_snapshot_t system_state;
int reached_hash(xbt_state_t st);
void set_pair_reached_hash(xbt_state_t st);
int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2);
-int data_program_region_compare(void *d1, void *d2, size_t size);
-int data_libsimgrid_region_compare(void *d1, void *d2, size_t size);
void MC_pair_delete(mc_pair_t pair);
void MC_exit_liveness(void);
mc_state_t MC_state_pair_new(void);
void MC_pair_stateless_delete(mc_pair_stateless_t pair);
/********************************** Configuration of MC **************************************/
-
-extern int _surf_do_mc_checkpoint;
extern xbt_fifo_t mc_stack_safety;
+extern int _surf_mc_checkpoint;
+extern char* _surf_mc_property_file;
+
+/****** Core dump ******/
+
+int create_dump(int pair);
+
#endif