Check aliasing constraints in PredicateCPA
Original issue created by @PhilippWendler on 2017-02-08 at 09:52:00, last modified on 2018-06-25 at 11:03:38
Similarly to #294 (closed), there may be other cases where the PredicateCPA's alias handling is too strict and prevents allowed aliasing as defined in C11 §6.5 (7). This should be checked in the C standard. For example, enum types are allowed to be aliased with ints because they are compatible (§6.7.2.2 (4)).
The exception is aliasing of arbitrary pointers to char
pointers, which is known to be allowed but the PredicateCPA cannot support it without giving up the idea of a type-segmented heap completely.
The concept of which types are allowed to be aliased should be generalized and moved out of the predicates
package. This can be based on the existing CTypes.areTypesCompatible
method.