Static code analysis / Code annotations

Question

I am writing code which is working like a state machine. So:

• some functions are setting a specific state
• others are allowed to be executed in a specific state.

(In reality it is a little more complex, but these are the basics, to keep it simple.)

Currently I use runtime assertions to check if a function is allowed in the current state. This is nice because it is kind of self documenting; moreover I can stop with the debugger on an assert and know where the error is. But the drawback is that it requires compiling the code, and that during testing I need to find custom inputs to fire the appropriate assertions.

Incidentally, I know that the Windows WDK provides annotations such as:

__drv_maxIRQL
__drv_setsIRQL

These annotations are statically checked using PreFAST, which can fire an error if necessary. This kind of static verification of code specifications is exactly what I need.

So the question is: are there any tools out there which provide similar functionality for programs specified in the form of state machines?

Answer 1

The Frama-C plug-in Aoraï does more or less exactly what you describe, for C programs, with the possibility of static verification. It does not rely on PreFAST but on comparable verification tools from the Frama-C platform.

• ConfusedSushi: Preferable is a solution for C++. But I will have a look on it.