Alias plugin does not propagate inside records and arrays
The Alias plug-in does not seem to know that if p
points to x
, then x.ptr
and p->ptr
are the same. This is also the case for pointers to arrays of pointers (with *(*)[]
types).
The attached files should reproduce the issue; when running them through frama-c -alias
I get
[alias] May-aliases at the end of function main:
{ a; t.field } { z; q } { z->field; b } { q->field; n }
which places the pointers a
, b
and n
in different classes even though we can check by running the program that a == b
and a == n
hold at the end of the main
function.
Note that in the plug-in's README, "pointer arithmetic, and array and structure accesses" is listed under "imprecisely-supported constructs", so this may be expected — however it would be surprising to me that "imprecisely-supported" means "unsound".