+/** 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;
+
} s_mc_snapshot_t, *mc_snapshot_t;
/** Information about a given stack frame
} 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;
}s_mc_visited_state_t, *mc_visited_state_t;
extern xbt_dynar_t visited_states;
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);
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);