--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Reduce number of Postconditions with assert



> However, when I try to compile the file, I get the following error:
> "Error during analysis of annotation: \old undefined in this context"

When you encounter this message, it is worth trying to substitute
"\at(e,Pre)" to "\old(e)".

Besides, you mention code with long sequences of ifs, so I would just
like to make sure that you are aware of the option "-why-opt
-fast-wp", an often recurring subject of this list (poorly indexed by
Google, I must say: I can't find a message with a good explanation,
but I know there are at least two, and probably more, in the
archives).

Pascal