size_t size;
} s_mc_mem_region_t, *mc_mem_region_t;
+/** Ignored data
+ *
+ * Some parts of the snapshot are ignored by zeroing them out: the real
+ * values is stored here.
+ * */
+typedef struct s_mc_snapshot_ignored_data {
+ void* start;
+ size_t size;
+ void* data;
+} s_mc_snapshot_ignored_data_t, *mc_snapshot_ignored_data_t;
+
typedef struct s_mc_snapshot{
size_t heap_bytes_used;
mc_mem_region_t regions[NB_REGIONS];
- int nb_processes;
+ xbt_dynar_t enabled_processes;
mc_mem_region_t* privatization_regions;
int privatization_index;
size_t *stack_sizes;
xbt_dynar_t stacks;
xbt_dynar_t to_ignore;
uint64_t hash;
+ xbt_dynar_t ignored_data;
} s_mc_snapshot_t, *mc_snapshot_t;
/** Information about a given stack frame
}s_mc_visited_state_t, *mc_visited_state_t;
extern xbt_dynar_t visited_states;
-int is_visited_state(void);
+mc_visited_state_t is_visited_state(void);
void visited_state_free(mc_visited_state_t state);
void visited_state_free_voidp(void *s);
void *data;
}s_mc_comm_pattern_t, *mc_comm_pattern_t;
+extern xbt_dynar_t initial_communications_pattern;
extern xbt_dynar_t communications_pattern;
extern xbt_dynar_t incomplete_communications_pattern;
void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
void MC_pre_modelcheck_comm_determinism(void);
+void MC_modelcheck_comm_determinism(void);
/* *********** Sets *********** */