さまざまな理由から、オフセットが 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;
ソースコードやプログラムの仕様を変更せずにこのプログラムを検証する方法はありますか? 読み取りを完了するにはどうすればよいですか?