問題タブ [verifiable-c]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
c - 非標準の呼び出し規約で VST forward_call が失敗する
VST 2.5 と Coq 8.11.0 を使用しています
forward_call非標準の呼び出し規則で関数を実行中にエラーが発生しました。最小限のコード例:
VST 仕様:
エラー：
これがバグなのか意図した動作なのかわかりませんので、いくつか質問があります。
1) これはバグですか?
2) そうでない場合、そのようなケースを証明するための回避策はありますか?
アップデート：
構造体コピーの制限を回避する次の回避策を使用した後、この問題に遭遇しましたstruct_normalize : statement -> statement。構造体の割り当てをフィールドごとの割り当てに置き換える関数を Coq で定義します。したがって、呼び出している関数に構造体のコピーがないという前提で作業しています。つまり、test_aux上記の例から を確認できます。質問は次のとおりです。
forward_call失敗するcc_structret := trueのはtest_auxASTだけですか?関数を正規化し、関数の本体から構造のコピーを削除した場合、それ
structretに応じて値を変更して証明を進めることは安全ですか?
c - VSTタイプのパニング
C ISO 99 標準は、いわゆる「型パニング」をサポートしています。以下に小さな例を示します。
ご覧のとおり、ここではユニオン型を使用constして、同じ型でconst.
VST:
この coq コードを実行すると、union から初期化されたフィールドを取得しようとしているかどうかを VST がチェックする証明不能なゴール (コメントに記載) に到達します。次のようになります。
戦術Falseによって変身します。entailer!
したがって、質問は次のとおりです。1) VST が和集合を互いに素な合計として表すのはなぜですか?
2) この機能 (型パニング) は VST でサポートされていませんか?
3) C コードの編集以外で、この問題を回避する方法はありますか?
c - VST でポインタのオフセット 0 から読み取ることができません
さまざまな理由から、オフセットが 0 のポインターから読み取ろうとするプログラムを検証しています。
VST でこれを確認すると、コンテキストは、ヒープのこの場所に値があることを前提としています。
ただし、forward読み取りを実行しようとすると、証明がエラーでスタックします。
しかし、前提条件を次のように調整すると、同じ読み取りがうまくいきます
または、読み取りが代わりになるようにソースコードを変更します。
ソースコードやプログラムの仕様を変更せずにこのプログラムを検証する方法はありますか? 読み取りを完了するにはどうすればよいですか?