@@ -40,46 +40,6 @@ void local_value_sett::make_union_adjusting_evs_types(
40
40
}
41
41
}
42
42
43
- std::pair<value_sett::valuest::iterator, bool >
44
- local_value_sett::init_per_field_external_value_set (
45
- const external_value_set_exprt &evse)
46
- {
47
- PRECONDITION (!evse.access_path_entries ().empty ());
48
- const typet &declared_on_type =
49
- evse.access_path_entries ().back ().declared_on_type ();
50
- std::string basename = evse.get_access_path_basename (declared_on_type);
51
- std::string access_path_suffix=evse.get_access_path_suffix ();
52
- std::string entryname=basename+access_path_suffix;
53
-
54
- entryt entry (basename, access_path_suffix, declared_on_type, evse);
55
-
56
- auto insert_result=values.insert (std::make_pair (irep_idt (entryname), entry));
57
-
58
- if (insert_result.second )
59
- insert (insert_result.first ->second .object_map , evse.as_initializer ());
60
-
61
- return insert_result;
62
- }
63
-
64
- void local_value_sett::init_precise_external_value_set (
65
- const external_value_set_exprt &evse,
66
- object_mapt &dest)
67
- {
68
- PRECONDITION (!evse.access_path_entries ().empty ());
69
- const typet &declared_on_type =
70
- external_value_set_exprt::get_precise_evs_irep_id ();
71
- std::string basename = evse.get_access_path_basename (declared_on_type);
72
- std::string access_path_suffix = evse.get_access_path_suffix ();
73
- std::string entryname = basename + access_path_suffix;
74
-
75
- const irep_idt key (entryname);
76
-
77
- if (values.count (key))
78
- make_union (dest, values.at (key).object_map );
79
- else
80
- insert (dest, evse);
81
- }
82
-
83
43
// / Builds a version of expr suitable for alias-comparison
84
44
// / \param expr: The expression to be converted to the alias-uniform structure
85
45
// / \return expr without information which is irrelevant to alias-comparison
@@ -303,10 +263,27 @@ void local_value_sett::get_value_set_rec(
303
263
new_entry, external_value_set_typet::PER_FIELD);
304
264
new_ext_set.type ()=field_type.subtype ();
305
265
306
- // TODO: figure out how to do this sort of on-demand-insert
307
- // without such ugly const hacking:
308
- auto insert_result = (const_cast <local_value_sett *>(this ))
309
- ->init_per_field_external_value_set (new_ext_set);
266
+ std::string basename =
267
+ new_ext_set.get_access_path_basename (declared_on_type);
268
+ std::string entryname = basename + access_path_suffix;
269
+
270
+ entryt entry (
271
+ basename, access_path_suffix, declared_on_type, new_ext_set);
272
+
273
+ // / If there is already an entry for this EVS then find it, otherwise
274
+ // / create a new entry for it
275
+ // / TODO: figure out how to do this sort of on-demand-insert
276
+ // / without such ugly const hacking:
277
+ auto insert_result =
278
+ (const_cast <local_value_sett *>(this ))
279
+ ->values .insert (std::make_pair (irep_idt (entryname), entry));
280
+
281
+ // / If we've just created a new entry then populate the object map
282
+ // / with an initializer EVS
283
+ if (insert_result.second )
284
+ insert (
285
+ insert_result.first ->second .object_map ,
286
+ new_ext_set.as_initializer ());
310
287
311
288
make_union (dest, insert_result.first ->second .object_map );
312
289
}
@@ -329,10 +306,21 @@ void local_value_sett::get_value_set_rec(
329
306
{
330
307
new_ext_set.type ()=field_type.subtype ();
331
308
332
- // TODO: figure out how to do this sort of on-demand-insert
333
- // without such ugly const hacking:
334
- (const_cast <local_value_sett *>(this ))
335
- ->init_precise_external_value_set (new_ext_set, dest);
309
+ declared_on_type =
310
+ external_value_set_exprt::get_precise_evs_irep_id ();
311
+ std::string basename =
312
+ new_ext_set.get_access_path_basename (declared_on_type);
313
+ access_path_suffix = new_ext_set.get_access_path_suffix ();
314
+ std::string entryname = basename + access_path_suffix;
315
+
316
+ const auto it = values.find (entryname);
317
+
318
+ // / If an entry already exists then use the values in the object
319
+ // / map, otherwise do not create an entry and use the EVS
320
+ if (it != values.end ())
321
+ make_union (dest, it->second .object_map );
322
+ else
323
+ insert (dest, new_ext_set);
336
324
}
337
325
}
338
326
}
0 commit comments