-/** \brief Fill/lookup the "subtype" field.
- */
-static void MC_resolve_subtype(mc_object_info_t info, dw_type_t type) {
-
- if(type->dw_type_id==NULL)
- return;
- type->subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
- if(type->subtype==NULL)
- return;
- if(type->subtype->byte_size != 0)
- return;
- if(type->subtype->name==NULL)
- return;
- // Try to find a more complete description of the type:
- // We need to fix in order to support C++.
-
- dw_type_t subtype = xbt_dict_get_or_null(info->full_types_by_name, type->subtype->name);
- if(subtype!=NULL) {
- type->subtype = subtype;
+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);
+
+ // Read smpi_privatisation_regions from MCed:
+ smpi_privatisation_region_t remote_smpi_privatisation_regions;
+ MC_process_read_variable(&mc_model_checker->process,
+ "smpi_privatisation_regions",
+ &remote_smpi_privatisation_regions, sizeof(remote_smpi_privatisation_regions));
+ s_smpi_privatisation_region_t privatisation_regions[process_count];
+ MC_process_read_simple(&mc_model_checker->process, &privatisation_regions,
+ remote_smpi_privatisation_regions, sizeof(privatisation_regions));
+
+ 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,
+ privatisation_regions[i].address, size,
+ ref_subreg);