@@ -369,67 +369,6 @@ void value_sett::get_value_set(
369
369
#endif
370
370
}
371
371
372
- // / Builds a version of expr suitable for alias-comparison
373
- // / \param expr: The expression to be converted to the alias-uniform structure
374
- // / \return expr without information which is irrelevant to alias-comparison
375
- static exprt get_uniform_expr (const exprt &expr)
376
- {
377
- if (expr.id ()==ID_object_descriptor)
378
- {
379
- object_descriptor_exprt ob;
380
- ob.object () = get_uniform_expr (to_object_descriptor_expr (expr).object ());
381
- ob.offset () = to_object_descriptor_expr (expr).offset ();
382
- return ob;
383
- }
384
- if (expr.id ()==ID_external_value_set)
385
- {
386
- exprt copy = expr;
387
- copy.set (ID_is_initializer, ID_0);
388
- return copy;
389
- }
390
- return expr;
391
- }
392
-
393
- // / Reconstructs a type of a pointer to the object expr
394
- // / \param expr: An object in a points-to set we make an alias type for
395
- // / \return A type of a pointer to the object expr
396
- static typet get_alias_type (const exprt &expr)
397
- {
398
- if (expr.id ()==ID_object_descriptor)
399
- {
400
- object_descriptor_exprt ob_expr=to_object_descriptor_expr (expr);
401
- if (ob_expr.offset ().id ()==ID_invalid || ob_expr.offset ().id ()==ID_unknown)
402
- return pointer_type (ob_expr.object ().type ());
403
- }
404
- return pointer_type (expr.type ());
405
- }
406
-
407
- void value_sett::get_may_alias_set (
408
- const exprt &expr,
409
- value_setst::valuest &dest,
410
- const namespacet &ns) const
411
- {
412
- object_mapt pointed_objects;
413
- get_value_set (expr, pointed_objects, ns, false );
414
- std::vector<exprt> uniform_pointed_objects;
415
- for (const auto &num_obj : pointed_objects.read ())
416
- uniform_pointed_objects.push_back (get_uniform_expr (to_expr (num_obj)));
417
-
418
- for (const auto &name_entry : values)
419
- for (const auto &enum_eobj : name_entry.second .object_map .read ())
420
- {
421
- if (std::find (uniform_pointed_objects.cbegin (),
422
- uniform_pointed_objects.cend (),
423
- get_uniform_expr (to_expr (enum_eobj)))!=
424
- uniform_pointed_objects.cend ())
425
- {
426
- dest.push_back (symbol_exprt (
427
- name_entry.second .identifier ,
428
- get_alias_type (to_expr (enum_eobj))));
429
- }
430
- }
431
- }
432
-
433
372
void value_sett::get_value_set (
434
373
const exprt &expr,
435
374
object_mapt &dest,
0 commit comments