問題タブ [abstract-interpretation]

私は抽象解釈のコースを受講していますが、理論が実際のコードにどのようにマッピングされるかの例を見たことがありません。

できればコンパイラ全体を操作する必要のない短いコード例を探しています。分析が有用である必要はありません。分析が導出されてから実装される例を見たいだけです。

おそらく大学のコースから、そのような例を知っている人はいますか?

形式手法に関する論文で「ループを折りたたんで終了させる必要がある」（正確には抽象解釈）に出くわしました。終了の意味はわかりますが、折り畳まれたループとは何か、ループで折り畳みを実行する方法もわかりません。

誰かが私に折り畳まれたループが何であるかを説明してもらえますか？そして、それが暗黙的ではない場合、または折り畳まれたループの定義にすぐに従わない場合、これはどのように終了を保証しますか？

ありがとう

データ フロー分析と抽象解釈の違いは何ですか?また、同じ目的で使用されますか? これら 2 つの相互の長所と短所は何ですか。

ユーザーヒントなしでループで拡張を実行する方法を探しています。例を使って説明します：

このコードで frama-c 値解析を実行すると、グローバル変数zは間隔 [--,--] を受け取ります。z がゼロに設定され、ループがインクリメンタル演算子で構成されているため、自動拡張メソッドは、より正確な間隔が [0, --] であると推定できるはずです。Frama-Cでこれを行うことは可能ですか?

次のコード サンプルがあるとします。

frama-c 値分析ツールを実行することで、a() の結果の間隔を推測でき、予想どおり [-50, 5100] であることが判明しました。ここで計算したいのは、a() の関数の要約、つまり入力と出力の関係です。上記の例で探している結果は、次のようになります。

私はコンテキストベースの要約に興味があるので、関数 a() の他のケースはあまり興味がないことに注意してください。

これを達成するための最良の方法は何ですか？

これが私の例です：

私がやりたいのは、メインで初期化されたときに入力変数 n の範囲を見つけて、関数 sum に到達することです。この例の正しい範囲は [1, 10] です。

このサンプルでは、​​元の入力をグローバル値に「保存」し、それを変数log_globalに割り当てて関数 sum に再導入し、関数に到達した元の入力を検出したいと考えています。このサンプルで frama-c を実行すると、log_input の範囲が [5, 14] で、log_global の範囲が [-10, 10] であることがわかります。これが発生する理由を理解しています. inの値はmainの開始時に設定され、nをさらに操作しても影響を受けません。

これをframa-cで変更する簡単な方法があるかどうか疑問に思っていましたか? おそらく、frama-c のコードの単純な変更でしょうか?

私が持っていた無関係なアイデアの 1 つは、メインの if ステートメントを操作することでした。

nの代わりにグローバル変数を使用しました。これは確かに正しい範囲になりますが、このソリューションは、より複雑な関数やより深い呼び出しスタックにうまく拡張できません。