静态代码分析/代码注释

Question

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

• 某些功能设置特定状态
• 人被允许在特定状态下执行。

（在现实中，它是一个有点复杂，但这些都是基本知识，以保持它的简单。）

目前我使用运行时断言检查，如果一个功能是允许在当前状态。这很好，因为它是一种自我记录;此外，我可以通过调试器停止断言并知道错误在哪里。但缺点是它需要编译代码，并且在测试过程中我需要找到自定义输入来触发相应的断言。

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

__drv_maxIRQL 
__drv_setsIRQL 

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

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

Answer 1

对于C程序，Frama-C插件Aoraï所做的或多或少与您所描述的内容完全相同，并且可以进行静态验证。它不依赖于PreFAST，而是依赖于Frama-C平台的可比较验证工具。