Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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