静态代码分析/代码注释

Question

我正在编写像状态机一样工作的代码。所以：

• 有些函数正在设置特定的状态。
• 其他的则允许在特定的状态下执行。

(实际上，这有点复杂，但这些都是保持简单的基本要素。)

目前，我使用运行时断言来检查函数是否允许处于当前状态。这很好，因为这是一种自我记录；此外，我可以停止使用断言上的调试器，并知道错误在哪里。但是缺点是，它需要编译代码，而且在测试期间，我需要找到自定义输入来触发适当的断言。

顺便说一句，我知道Windows WDK提供了一些注释，如：

__drv_maxIRQL
__drv_setsIRQL

使用PreFAST静态地检查这些注释，如果有必要，会触发错误。这种静态的代码规范验证正是我所需要的。

因此，问题是:是否有任何工具为以状态机形式指定的程序提供类似的功能？

Answer 1

Frama插件奥拉或多或少地完成了您对C程序的描述，并提供了静态验证的可能性。它不依赖于PreFAST，而是依赖于来自Frama平台的可比验证工具。