Sound aliasing with char pointers in PredicateCPA
Original issue created by @PhilippWendler on 2017-02-08 at 10:01:52, last modified on 2017-02-08 at 10:01:52
As stated in #295, accessing memory of other types through char
pointers is legal in C, but it is currently not supported by the PredicateCPA.
One idea how to make this at least sound is that whenever a write to e.g. an int
pointer is done, we simulate another write of non-deterministic bytes through a char
pointer. And if a write through a char
pointer is done, we similarly set the respective memory cells for all other types to non-deterministic.
This is a little bit expensive because when not using quantifiers or arrays for the heap, a pointer write can mean creating a large formula, but maybe the cost is acceptable (we should at least have such an option).