問題タブ [value-analysis]

次の C コードがあるとします。

初期化時に変数 x の境界を静的分析を使用して計算したいと思います。これにより、満足のいく述語が得られます。この例では、メインの開始時の x の間隔は [8, 12] である必要があります。

TL;DR:コードのどこかにアサーションがある場合、これらの範囲を計算する最良の方法は何ですか?

私がこれまでに試したこと：

これにアプローチする最善の方法は、最も弱い前提条件計算機を使用することだと思います。私は frama-c の wp プラグインをいじってみましたが、検証目的で構築されているため、このユース ケースでどれほど役立つかはわかりません。次のコードにプラグインを適用する場合:

次の述語が代替エルゴ ソルバーに送信されます。

注意深く見ると、結果が (i_1 = 0) にならない変数 i の境界に従うことで、入力に必要な間隔を識別することができます。私はこれらの境界をマークしました。これはあまり堅牢ではありません。たとえば、アサーションが&& n <= 13に変更された場合、暗黙の述語の「左側」は変更された条件がないため同じままです。また、関数を呼び出すときにアサーションをrequireステートメントに変更するなど、他のシナリオでこれがどれほど役立つかはわかりませんが、結果の述語を理解できません:

そして、require ステートメントを関数に追加します。

私は得る：

値分析を使用して、Frama-C のプラグインに取り組んでいます。各ステートメントの後に変数（値）の状態を出力したいだけです（解決策は簡単だと思いますが、わかりませんでした）。

ビジターDb.Value.get_stmt_state内のメソッドで現状を取得しました。vstmt_aux

変数の値を取得するにはどうすればよいですか?

PS: この投稿を見つけましたが、役に立ちませんでした。実際の解決策はありません。説明の助けを借りて、それを行うことができませんでした: Value.Eval_expr、Value.Eval_op などのモジュールで関数を使用する方法Frama-c Value プラグイン

私は Frama-C-Plugin を開発しています。これは、各ステートメントの後に変数の値を出力する必要があります。Frama-C-Gui の [Values] タブで、プログラム全体の分析値と、さまざまな関数呼び出しの後で (関数のパラメーターを使用して) 分析値を確認できます。

私は今、各関数呼び出しの後に値を取得したいと考えています(「すべて」の行ではなく、「メイン」の行です。

スクリーンショットに使用したプログラムは次のとおりです。

これは可能ですか？これらの値にアクセスするにはどうすればよいですか?

PS: 関連する質問をしましたが、既に「すべて」の部分 (およびステートメントの前の値) が出力されています。次のリンクを参照してください: Frama-C Plugin development: Getting result of value-analysis

同様の解決策はありますか？