+static xbt_dynar_t MC_get_local_variables_values(xbt_dynar_t stack_frames)
+{
+
+ unsigned cursor1 = 0;
+ mc_stack_frame_t stack_frame;
+ xbt_dynar_t variables =
+ xbt_dynar_new(sizeof(local_variable_t), local_variable_free_voidp);
+
+ xbt_dynar_foreach(stack_frames, cursor1, stack_frame) {
+ mc_fill_local_variables_values(stack_frame, stack_frame->frame, variables);
+ }
+
+ return variables;
+}
+
+static void MC_stack_frame_free_voipd(void *s)
+{
+ mc_stack_frame_t stack_frame = *(mc_stack_frame_t *) s;
+ if (stack_frame) {
+ xbt_free(stack_frame->frame_name);
+ xbt_free(stack_frame);
+ }
+}
+
+static xbt_dynar_t MC_unwind_stack_frames(void *stack_context)
+{
+ xbt_dynar_t result =
+ xbt_dynar_new(sizeof(mc_stack_frame_t), MC_stack_frame_free_voipd);
+
+ unw_cursor_t c;
+
+ // TODO, check condition check (unw_init_local==0 means end of frame)
+ if (unw_init_local(&c, (unw_context_t *) stack_context) != 0) {
+
+ xbt_die("Could not initialize stack unwinding");
+
+ } else
+ while (1) {
+
+ mc_stack_frame_t stack_frame = xbt_new(s_mc_stack_frame_t, 1);
+ xbt_dynar_push(result, &stack_frame);
+
+ stack_frame->unw_cursor = c;
+
+ unw_word_t ip, sp;
+
+ unw_get_reg(&c, UNW_REG_IP, &ip);
+ unw_get_reg(&c, UNW_REG_SP, &sp);
+
+ stack_frame->ip = ip;
+ stack_frame->sp = sp;
+
+ // TODO, use real addresses in frame_t instead of fixing it here
+
+ dw_frame_t frame = MC_find_function_by_ip((void *) ip);
+ stack_frame->frame = frame;
+
+ if (frame) {
+ stack_frame->frame_name = xbt_strdup(frame->name);
+ stack_frame->frame_base =
+ (unw_word_t) mc_find_frame_base(frame, frame->object_info, &c);
+ } else {
+ stack_frame->frame_base = 0;
+ stack_frame->frame_name = NULL;
+ }
+
+ /* Stop before context switch with maestro */
+ if (frame != NULL && frame->name != NULL
+ && !strcmp(frame->name, "smx_ctx_sysv_wrapper"))
+ break;
+
+ int ret = ret = unw_step(&c);
+ if (ret == 0) {
+ xbt_die("Unexpected end of stack.");
+ } else if (ret < 0) {
+ xbt_die("Error while unwinding stack.");
+ }
+ }
+
+ if (xbt_dynar_length(result) == 0) {
+ XBT_INFO("unw_init_local failed");
+ xbt_abort();
+ }
+
+ return result;
+};
+
+static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t * snapshot)
+{
+
+ xbt_dynar_t res =
+ xbt_dynar_new(sizeof(s_mc_snapshot_stack_t),
+ MC_snapshot_stack_free_voidp);
+
+ unsigned int cursor = 0;
+ stack_region_t current_stack;
+
+ xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
+ mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
+ st->stack_frames = MC_unwind_stack_frames(current_stack->context);
+ st->local_variables = MC_get_local_variables_values(st->stack_frames);
+
+ unw_word_t sp = xbt_dynar_get_as(st->stack_frames, 0, mc_stack_frame_t)->sp;
+
+ xbt_dynar_push(res, &st);
+ (*snapshot)->stack_sizes =
+ xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
+ (*snapshot)->stack_sizes[cursor] =
+ (char*) current_stack->address + current_stack->size - (char*) sp;
+ }
+
+ return res;
+
+}
+
+static xbt_dynar_t MC_take_snapshot_ignore()
+{
+
+ if (mc_heap_comparison_ignore == NULL)
+ return NULL;
+
+ xbt_dynar_t cpy =
+ xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
+ heap_ignore_region_free_voidp);
+
+ unsigned int cursor = 0;
+ mc_heap_ignore_region_t current_region;
+
+ xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region) {
+ mc_heap_ignore_region_t new_region = NULL;
+ new_region = xbt_new0(s_mc_heap_ignore_region_t, 1);
+ new_region->address = current_region->address;
+ new_region->size = current_region->size;
+ new_region->block = current_region->block;
+ new_region->fragment = current_region->fragment;
+ xbt_dynar_push(cpy, &new_region);
+ }
+
+ return cpy;
+
+}
+
+static void mc_free_snapshot_ignored_data_pvoid(void* data) {
+ mc_snapshot_ignored_data_t ignored_data = (mc_snapshot_ignored_data_t) data;
+ free(ignored_data->data);
+}
+
+static void MC_snapshot_handle_ignore(mc_snapshot_t snapshot)
+{
+ snapshot->ignored_data = xbt_dynar_new(sizeof(s_mc_snapshot_ignored_data_t), mc_free_snapshot_ignored_data_pvoid);
+
+ // Copy the memory:
+ unsigned int cursor = 0;
+ mc_checkpoint_ignore_region_t region;
+ xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+ s_mc_snapshot_ignored_data_t ignored_data;
+ ignored_data.start = region->addr;
+ ignored_data.size = region->size;
+ ignored_data.data = malloc(region->size);
+ memcpy(ignored_data.data, region->addr, region->size);
+ xbt_dynar_push(snapshot->ignored_data, &ignored_data);
+ }
+
+ // Zero the memory:
+ xbt_dynar_foreach (mc_checkpoint_ignore, cursor, region) {
+ memset(region->addr, 0, region->size);
+ }
+
+}
+
+static void MC_snapshot_ignore_restore(mc_snapshot_t snapshot)
+{
+ unsigned int cursor = 0;
+ s_mc_snapshot_ignored_data_t ignored_data;
+ xbt_dynar_foreach (snapshot->ignored_data, cursor, ignored_data) {
+ memcpy(ignored_data.start, ignored_data.data, ignored_data.size);
+ }
+}
+
+/** @brief Can we remove this snapshot?
+ *
+ * Some snapshots cannot be removed (yet) because we need them
+ * at this point.
+ *
+ * @param snapshot
+ */
+int mc_important_snapshot(mc_snapshot_t snapshot)
+{
+ // We need this snapshot in order to know which
+ // pages needs to be stored in the next snapshot:
+ if (_sg_mc_sparse_checkpoint && snapshot == mc_model_checker->parent_snapshot)
+ return true;
+
+ return false;
+}
+
+mc_snapshot_t MC_take_snapshot(int num_state)
+{
+
+ mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
+ snapshot->enabled_processes = xbt_dynar_new(sizeof(int), NULL);
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list) {
+ xbt_dynar_push_as(snapshot->enabled_processes, int, (int)process->pid);
+ }
+
+ MC_snapshot_handle_ignore(snapshot);
+
+ /* Save the std heap and the writable mapped pages of libsimgrid and binary */
+ MC_get_memory_regions(snapshot);
+ if (_sg_mc_sparse_checkpoint && _sg_mc_soft_dirty) {
+ mc_softdirty_reset();
+ }
+
+ snapshot->to_ignore = MC_take_snapshot_ignore();
+
+ if (_sg_mc_visited > 0 || strcmp(_sg_mc_property_file, "")) {
+ snapshot->stacks =
+ MC_take_snapshot_stacks(&snapshot);
+ if (_sg_mc_hash && snapshot->stacks != NULL) {
+ snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks);
+ } else {
+ snapshot->hash = 0;
+ }
+ } else {
+ snapshot->hash = 0;
+ }
+
+ MC_snapshot_ignore_restore(snapshot);
+ mc_model_checker->parent_snapshot = snapshot;
+ return snapshot;
+}
+
+void MC_restore_snapshot(mc_snapshot_t snapshot)