Description
Note: This issue references functionality that's currently not merged into develop.
This is how other subdomains of VSD work (see e.g. constant_abstract_objectt
vs constant_pointer_abstract_objectt
). As of now this is causing problems with merging, because the set management uses pointer comparisons to determine if two objects are equal (e.g. if you have two value sets each consisting only of pointer-to-three, you'll end up with a value set with two different pointer-to-three's in it).
What should be done instead is that value_set_abstract_objectt
should only manage exprt
s, and for pointers we either use constant_pointer_abstract_objectt
or add a set_pointer_abstract_objectt
that manages a set of possible pointees to complement the value set. Possibly similar considerations for arrays.