靜態代碼分析/代碼註釋

Question

我正在編寫像狀態機一樣工作的代碼。所以：

• 某些功能設置特定狀態
• 人被允許在特定狀態下執行。

（在現實中，它是一個有點複雜，但這些都是基本知識，以保持它的簡單。）

目前我使用運行時斷言檢查，如果一個功能是允許在當前狀態。這很好，因爲它是一種自我記錄;此外，我可以通過調試器停止斷言並知道錯誤在哪裏。但缺點是它需要編譯代碼，並且在測試過程中我需要找到自定義輸入來觸發相應的斷言。

順便說一句，我知道，在Windows WDK提供了註釋，比如：

__drv_maxIRQL 
__drv_setsIRQL 

這些註釋使用PreFAST，如果必要的話，可以觸發一個錯誤靜態檢查。代碼規範的這種靜態驗證正是我所需要的。

所以問題是：是否有任何工具提供類似的功能，以狀態機的形式指定的程序？

Answer 1

對於C程序，Frama-C插件Aoraï所做的或多或少與您所描述的內容完全相同，並且可以進行靜態驗證。它不依賴於PreFAST，而是依賴於Frama-C平臺的可比較驗證工具。