+ size_t process_count = smpi_process_count();
+ mc_mem_region_t region = xbt_new(s_mc_mem_region_t, 1);
+ region->region_type = region_type;
+ region->storage_type = MC_REGION_STORAGE_TYPE_PRIVATIZED;
+ region->start_addr = start_addr;
+ region->permanent_addr = permanent_addr;
+ region->size = size;
+ region->privatized.regions_count = process_count;
+ region->privatized.regions = xbt_new(mc_mem_region_t, process_count);
+
+ for (size_t i = 0; i < process_count; i++) {
+ mc_mem_region_t ref_subreg = NULL;
+ if (ref_reg && ref_reg->storage_type == MC_REGION_STORAGE_TYPE_PRIVATIZED)
+ ref_subreg = ref_reg->privatized.regions[i];
+ region->privatized.regions[i] =
+ MC_region_new(region_type, start_addr,
+ MC_privatization_address(&mc_model_checker->process, i), size,
+ ref_subreg);
+ }
+
+ return region;
+}
+
+static void MC_snapshot_add_region(int index, mc_snapshot_t snapshot, mc_region_type_t type,
+ mc_object_info_t object_info,
+ void *start_addr, void* permanent_addr, size_t size)
+{
+ if (type == MC_REGION_TYPE_DATA)
+ xbt_assert(object_info, "Missing object info for object.");
+ else if (type == MC_REGION_TYPE_HEAP)
+ xbt_assert(!object_info, "Unexpected object info for heap region.");
+
+ mc_mem_region_t ref_reg = NULL;
+ if (mc_model_checker->parent_snapshot)
+ ref_reg = mc_model_checker->parent_snapshot->snapshot_regions[index];
+
+ mc_mem_region_t region;
+ const bool privatization_aware = MC_object_info_is_privatized(object_info);
+ if (privatization_aware && smpi_process_count())
+ region = MC_region_new_privatized(type, start_addr, permanent_addr, size, ref_reg);
+ else
+ region = MC_region_new(type, start_addr, permanent_addr, size, ref_reg);
+
+ region->object_info = object_info;
+ snapshot->snapshot_regions[index] = region;