Cプログラムの静的不変発見ツールはありますか？

Question

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

私が探しているツールはありますか？ありがとう！

Answer 1

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

Frama-Cの価値分析は、それぞれのステートメントのすべての変数の可能な値であるその結果を累積します。分析の終わりには、それにより、各ステートメントで、プログラム内の各変数のドメイン変動に関する非関係情報を提示することができます。 this screenshotでは、この確定的プログラムのすべての実行に対して、選択された命令の直前にはSが常に0,1,3または6であることが不変である。

問題の2つの隠れたパラメータは、あなたが興味を持っている不変量の形と、これらの不変量を見つけるプログラムの形です。たとえば、Iraの回答に記載されているSLAMは、デバイスドライバのコードを処理し、システムAPIの適切な使用を検証するために必要な情報だけを含む不変量を推測するように設計されています。別のツールAstréeは、飛行制御ソフトウェアの実行時の安全性を実証するための正しい不変量を推論する上で非常に良い仕事をしていることで有名です。

2自由度は非常に大きな設計スペースになります。すべての種類のCプログラムに対応するものは見つからず、関心のある不変条件を推論しますが、特定のアプリケーションドメインと不変条件について質問を絞り込むと、関連する回答を見つける機会が増えます。

Answer 2

The SLAM project: debugging system software via static analysisを参照してください。それは不変量を静的に推論すると主張していますが、C言語です。著者Tom Ballは、プログラム分析における恒星研究として広く知られています。