@@ -338,92 +338,99 @@ void local_value_sett::apply_assign_side_effects(
338
338
const exprt &rhs,
339
339
const namespacet &ns)
340
340
{
341
- if (rhs.id ()==ID_side_effect &&
342
- rhs.get (ID_statement)==ID_allocate)
341
+ if (rhs.id () == ID_side_effect && rhs.get (ID_statement) == ID_allocate)
342
+ demote_most_recent_dynamic_objects (location_number);
343
+ }
344
+
345
+ void local_value_sett::demote_most_recent_dynamic_objects (
346
+ const unsigned loc_number)
347
+ {
348
+ // Replace all the current most-recent-allocation dynamic-objects
349
+ // with the corresponding any-allocation ones
350
+ for (auto &value : values)
343
351
{
344
- const typet &dynamic_type=
345
- static_cast < const typet &>(rhs. find (ID_C_cxx_alloc_type) );
352
+ entryt &entry = value. second ;
353
+ object_map_dt &object_map = entry. object_map . write ( );
346
354
347
- // Replace all the current most-recent-allocation dynamic-objects
348
- // with the corresponding any-allocation ones
349
- for (auto &value : values)
350
- {
351
- entryt &entry=value.second ;
352
- object_map_dt &object_map=entry.object_map .write ();
353
-
354
- // Look-up for the first appearance of the current
355
- // most-recent dynamic-object in the current object-map
356
- object_map_dt::iterator it=boost::range::find_if (
357
- object_map,
358
- [this ] (const object_map_dt::value_type &object)
359
- {
360
- const exprt &o=object_numbering[object.first ];
361
- if (o.id ()!=ID_dynamic_object)
362
- return false ;
355
+ // Look-up for the first appearance of the current
356
+ // most-recent dynamic-object in the current object-map
357
+ object_map_dt::iterator it = boost::range::find_if (
358
+ object_map, [this , loc_number](const object_map_dt::value_type &object) {
359
+ const exprt &o = object_numbering[object.first ];
360
+ if (o.id () != ID_dynamic_object)
361
+ return false ;
363
362
364
- const dynamic_object_exprt &dynamic_object= to_dynamic_object_expr (o);
363
+ const dynamic_object_exprt &dynamic_object = to_dynamic_object_expr (o);
365
364
366
- return dynamic_object.get_instance ()==location_number &&
367
- dynamic_object.get_recency ()==
368
- dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION;
369
- });
365
+ return dynamic_object.get_instance () == loc_number &&
366
+ dynamic_object.get_recency () ==
367
+ dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION;
368
+ });
370
369
371
- if (it== object_map.end ())
372
- continue ;
370
+ if (it == object_map.end ())
371
+ continue ;
373
372
374
- // Delete the most-recent dynamic-object from the current object_map
375
- object_map.erase (it);
373
+ // Delete the most-recent dynamic-object from the current object_map
374
+ object_map.erase (it);
376
375
377
- int index_dynamic_object_recent= it->first ;
376
+ const int index_dynamic_object_recent = it->first ;
378
377
379
- // Create the any-allocation dynamic-object
380
- // by copying the existing most-recent one and adjusting the recency flag
381
- dynamic_object_exprt dynamic_object_any_allocation=
382
- to_dynamic_object_expr (object_numbering[index_dynamic_object_recent]);
383
- dynamic_object_any_allocation.set_recency (false );
378
+ // Create the any-allocation dynamic-object
379
+ // by copying the existing most-recent one and adjusting the recency flag
380
+ dynamic_object_exprt dynamic_object_any_allocation =
381
+ to_dynamic_object_expr (object_numbering[index_dynamic_object_recent]);
382
+ dynamic_object_any_allocation.set_recency (false );
384
383
385
- // Add the newly created any-allocation dynamic-object
386
- // in the current rhs' object_map
387
- insert (entry.object_map , dynamic_object_any_allocation, 0 );
388
- }
384
+ // Add the newly created any-allocation dynamic-object
385
+ // in the current rhs' object_map
386
+ insert (entry.object_map , dynamic_object_any_allocation, 0 );
387
+ }
389
388
390
- const std::string name_most_recent=
391
- prefix_dynamic_object+
392
- std::to_string (location_number)+
393
- id2string (ID_most_recent_allocation);
394
- const std::string name_any_allocation=
395
- prefix_dynamic_object+
396
- std::to_string (location_number)+
397
- id2string (ID_any_allocation);
398
-
399
- // Iterates over the domain's entries and when we find the current
400
- // most-recent-allocation dynamic-object, add its object-map
401
- // to its correspondent any-allocation dynamic-object's object-map
402
- for (auto &value : values)
403
- {
404
- entryt &entry=value.second ;
389
+ const std::string name_most_recent = prefix_dynamic_object +
390
+ std::to_string (loc_number) +
391
+ id2string (ID_most_recent_allocation);
392
+ const std::string name_any_allocation = prefix_dynamic_object +
393
+ std::to_string (loc_number) +
394
+ id2string (ID_any_allocation);
395
+
396
+ // Iterates over the domain's entries and when we find the current
397
+ // most-recent-allocation dynamic-object, add its object-map to the
398
+ // corresponding any-allocation dynamic-object's object-map and remove it
399
+ // from the domain
400
+ std::vector<valuest::iterator> to_remove;
401
+ for (auto it = values.begin (); it != values.end (); ++it)
402
+ {
403
+ auto &value = *it;
404
+ entryt &entry = value.second ;
405
405
406
- if (entry.identifier ==name_most_recent)
407
- {
408
- DATA_INVARIANT (
409
- can_cast_expr<dynamic_object_exprt>(entry.structured_lhs ),
410
- " If identifier of entryt begins with dynamic object prefix then its "
411
- " structured_lhs should be castable to a dynamic_object_exprt" );
412
- dynamic_object_exprt expr_any_allocation =
413
- to_dynamic_object_expr (entry.structured_lhs );
414
- expr_any_allocation.set_recency (false );
415
-
416
- entryt &entry_any_allocation = get_entry (
417
- entryt (name_any_allocation, entry.suffix , expr_any_allocation),
418
- dynamic_type,
419
- ns);
420
-
421
- // Add into the any-allocation dynamic-object's object_map
422
- // the most-recent-allocation dynamic-object's object_map
423
- make_union (entry_any_allocation.object_map , entry.object_map );
424
- }
406
+ if (entry.identifier == name_most_recent)
407
+ {
408
+ DATA_INVARIANT (
409
+ can_cast_expr<dynamic_object_exprt>(entry.structured_lhs ),
410
+ " If identifier of entryt begins with dynamic object prefix then its "
411
+ " structured_lhs should be castable to a dynamic_object_exprt" );
412
+ dynamic_object_exprt expr_any_allocation =
413
+ to_dynamic_object_expr (entry.structured_lhs );
414
+ expr_any_allocation.set_recency (false );
415
+
416
+ // / The second and third arguments to get_entry() are only used for
417
+ // / field_sensitive(), and that will always returns true without using
418
+ // / them because name_any_allocation starts with the prefix for a
419
+ // / dynamic object, so we can use an empty type and namespace.
420
+ entryt &entry_any_allocation = get_entry (
421
+ entryt (name_any_allocation, entry.suffix , expr_any_allocation),
422
+ nil_typet (),
423
+ namespacet (symbol_tablet ()));
424
+
425
+ // Add into the any-allocation dynamic-object's object_map
426
+ // the most-recent-allocation dynamic-object's object_map
427
+ make_union (entry_any_allocation.object_map , entry.object_map );
428
+ to_remove.push_back (it);
425
429
}
426
430
}
431
+
432
+ for (auto it : to_remove)
433
+ values.erase (it);
427
434
}
428
435
429
436
void local_value_sett::demote_initializers (object_mapt &values_rhs) const
0 commit comments