@@ -173,12 +173,9 @@ void local_value_set_analysist::transform_function_stub(
173
173
std::map<exprt, local_value_sett::object_mapt> pre_call_rhs_value_sets;
174
174
const std::string per_field_evs_prefix=" external_objects" ;
175
175
176
- std::set<std::pair<std::string, std::string> > lhs_written;
177
-
178
176
for (const auto &assignment : assignments)
179
177
{
180
178
++nstub_assignments;
181
- const auto &lhs_fieldname=assignment.first ;
182
179
const auto &rhs_expr=assignment.second ;
183
180
if (pre_call_rhs_value_sets.count (rhs_expr))
184
181
continue ;
@@ -191,11 +188,6 @@ void local_value_set_analysist::transform_function_stub(
191
188
const std::string &evse_label=
192
189
id2string (to_constant_expr (evse.label ()).get_value ());
193
190
194
- // Differentiate external-set entries that only contain
195
- // their initialiser from ones that have been written:
196
- if (!evse.is_initializer ())
197
- lhs_written.insert ({lhs_fieldname.base_name , lhs_fieldname.field_name });
198
-
199
191
if (has_prefix (evse_label, per_field_evs_prefix))
200
192
{
201
193
// This external value set denotes either all pointers stored in a
@@ -275,7 +267,6 @@ void local_value_set_analysist::transform_function_stub(
275
267
// Ordinary value set member (not an external value set);
276
268
// just add to the RHS map.
277
269
valuesets.insert (rhs_map, rhs_expr);
278
- lhs_written.insert ({lhs_fieldname.base_name , lhs_fieldname.field_name });
279
270
}
280
271
}
281
272
@@ -295,12 +286,21 @@ void local_value_set_analysist::transform_function_stub(
295
286
const auto find_pair=std::make_pair (
296
287
lhs_fieldname.base_name ,
297
288
lhs_fieldname.field_name );
298
- if (lhs_written.count (find_pair))
289
+
290
+ const bool rhs_is_initializer_per_field_evs =
291
+ assignment.second .id () == ID_external_value_set &&
292
+ to_external_value_set (assignment.second )
293
+ .get_external_value_set_type () ==
294
+ external_value_set_typet::PER_FIELD &&
295
+ to_external_value_set (assignment.second ).is_initializer ();
296
+ if (!rhs_is_initializer_per_field_evs)
297
+ {
299
298
get_all_field_value_sets (
300
299
lhs_fieldname.field_name ,
301
300
lhs_fieldname.declared_on_type ,
302
301
valuesets,
303
302
lhs_entries);
303
+ }
304
304
305
305
// Also write to the external value set itself, representing writes
306
306
// whose effects are external to this context too:
0 commit comments