c2fsm is a translator for a fragment of ANSI C to an interpreted
automaton in the format of the FAST static analyzer. c2fsm
can be downloaded from here
3.2.1 Known bugs and problems
The translation of C contructs in which the result of a comparison
becomes a zero/one value (e.g. cmp = x <= y;
or cmp = x <= y? 1: 0;) is not compatible with the FAST syntax.
Replace by an explicit conditional: if(x<=y)cmp = 1 else cmp = 0;.
- The -v option (removal of useless variables) does not work.
Systematically replace i++ by ++i when possible.