For various reasons I am verifying a program that attempts to read from a pointer with an offset of 0:
int x = (*(z + 0)).ssl_int;
When verifying this in VST, the context has as an assumption that there is a value on the heap at this location:
data_at Tsh (Tunion _sslval noattr) (inr x2) z
However, when trying to run forward over the read, the proof gets stuck with the error:
It is not obvious how to move forward here. ...
But the same read goes through fine if I adjust my precondition to be
data_at Tsh (tarray (Tunion_sslval noattr) 1) [(inr x2)] z
or change the source code such that the read is instead:
int x = (*z).ssl_int;
Is there a way to verify this program without changing the source code or the program specification? How can I make the read go through?
