由于各种原因，我正在验证一个尝试从偏移量为 0 的指针读取的程序：
int x = (*(z + 0)).ssl_int;
在 VST 中验证这一点时，上下文假设在此位置的堆上有一个值：
data_at Tsh (Tunion _sslval noattr) (inr x2) z
但是，当尝试forward遍历读取时，证明卡住了错误：
It is not obvious how to move forward here. ...
但是如果我将前提条件调整为
data_at Tsh (tarray (Tunion_sslval noattr) 1) [(inr x2)] z
或更改源代码，以便改为：
int x = (*z).ssl_int;
有没有办法在不改变源代码或程序规范的情况下验证这个程序？我怎样才能让阅读通过？