+ }
+}
+
+// FIXME, multiple privatisation regions
+// FIXME, cross-process
+static inline
+void* MC_privatization_address(mc_process_t process, int process_index)
+{
+ xbt_assert(process_index >= 0);
+ return smpi_privatisation_regions[process_index].address;
+}
+
+static mc_mem_region_t MC_region_new_privatized(
+ mc_region_type_t region_type, void *start_addr, void* permanent_addr, size_t size,
+ mc_mem_region_t ref_reg)
+{
+ size_t process_count = MC_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 && MC_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;
+ return;
+}
+
+static void MC_get_memory_regions(mc_process_t process, mc_snapshot_t snapshot)
+{
+ const size_t n = process->object_infos_size;
+ snapshot->snapshot_regions_count = n + 1;
+ snapshot->snapshot_regions = xbt_new0(mc_mem_region_t, n + 1);
+
+ for (size_t i = 0; i!=n; ++i) {
+ mc_object_info_t object_info = process->object_infos[i];
+ MC_snapshot_add_region(i, snapshot, MC_REGION_TYPE_DATA, object_info,
+ object_info->start_rw, object_info->start_rw,
+ object_info->end_rw - object_info->start_rw);