【发布时间】：2012-03-12 17:29:42
【问题描述】：
我正在编写像状态机一样工作的代码。所以：
- 某些函数正在设置特定状态
- 允许在特定状态下执行其他操作。
（实际上它有点复杂，但为了保持简单，这些是基础知识。）
目前我使用运行时断言来检查当前状态下是否允许某个函数。这很好，因为它是一种自我记录；此外，我可以在断言上停止调试器并知道错误在哪里。但缺点是它需要编译代码，并且在测试期间我需要找到自定义输入来触发适当的断言。
顺便说一下，我知道 Windows WDK 提供了如下注释：
__drv_maxIRQL
__drv_setsIRQL
这些注解使用PreFAST 进行静态检查，必要时会引发错误。这种代码规范的静态验证正是我所需要的。
所以问题是：是否有任何工具可以为以状态机形式指定的程序提供类似的功能？
【问题讨论】：
标签： annotations static-analysis