--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on July 2010 ---
> 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