c - C プログラム用の静的不変検出ツールはありますか?

Question

C プログラムの不変条件を静的に発見できるツールを探しています。Daikonをチェックしましたが、不変条件は動的にしか検出されません。

私が探しているものに利用できるツールはありますか? ありがとう！

Answer 1

SLAM プロジェクト: 静的解析によるシステム ソフトウェアのデバッグを参照してください。それは、まさにあなたが求めていた C 言語に対して、不変条件を静的に推論すると主張しています。著者の Tom Ball は、プログラム分析の優れた業績で広く知られています。

Answer 2

Daikon にリンクされたページが使用しているように、最も広い意味で「不変」を意味する場合、多くの静的分析ツールの作業は「不変の発見」と表現できます。

Frama-C の値分析は、ステートメントごとに、その結​​果 (すべての変数の可能な値) を蓄積します。したがって、分析の最後に、各ステートメントで、プログラム内の各変数のドメイン変動に関する非関係情報を提示できます。このスクリーンショットでは、不変条件はS、この決定論的プログラムのすべての実行で、選択された命令の直前で常に 0、1、3、または 6 です。

質問の 2 つの隠しパラメーターは、関心のある不変条件の形状と、これらの不変条件を見つけたいプログラムの形状です。たとえば、Ira の回答で言及されている SLAM は、デバイス ドライバー コードで動作し、システム API の適切な使用を検証するために必要な情報だけを含む不変式を推論するように設計されています。もう 1 つのツールであるAstréeは、飛行制御ソフトウェアの実行時の安全性を実証するために、適切な不変条件を推測するのに非常に優れていることで有名です。

自由度が 2 であるため、設計空間が非常に大きくなります。すべての種類の C プログラムで機能し、関心のあるすべての不変条件を推測できるものは見つかりませんが、特定のアプリケーション ドメインと不変条件の種類について質問を絞り込むと、関連する回答を見つける可能性が高くなります。