スタティックコード解析/コード注釈

Question

私はステートマシンのように動作しているコードを書いています。だから、：

• 一部の機能は
• 他人が特定の状態で実行することが許可されている特定の状態に設定されています。

（現実には、それはもう少し複雑ですが、これらは基本です、それをシンプルに保つために。）

現在、私は、関数が現在の状態で許可されているかどうかを確認するために、ランタイム・アサーションを使用しています。これは自己文書化の一種であるため、これは素晴らしいことです。さらに、私はアサートでデバッガを停止し、エラーの原因を知ることができます。しかし、欠点は、コードのコンパイルが必要であり、テスト中に適切なアサーションを発生させるカスタム入力を見つける必要があるということです。これらのアノテーションは、静的に、必要に応じて、エラーを発射することができPreFASTを、使用してチェックされ

__drv_maxIRQL 
__drv_setsIRQL 

：

ところで、私は、WindowsのWDKのような注釈を提供することを知っています。この種のコード仕様の静的検証はまさに私が必要としているものです。

ステートマシンの形式で指定されたプログラムに同様の機能を提供するツールはありますか？

Answer 1

Frama-CプラグインAoraïは、静的検証の可能性があるCプログラムの場合、あなたが何を記述しているかを多かれ少なかれ正確に表します。 PreFASTに頼るのではなく、Frama-Cプラットフォームの同等の検証ツールに依存しています。