--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on September 2013 ---
Hello Virgile, Le 05/09/2013 13:11, Virgile Prevosto a ?crit : > There are two issues: first, it appears that (_?_:_) is not supported > by Value in predicate evaluation (it should not be too complicated to > fix, though). This can be overcome by splitting the ensures into two > implications. > The second point is more subtle: the 'x' in the post-condition is in > fact an '\old(x)', to account for the fact that formals in the > post-condition have their initial value. When Value sees this \old, it > evaluates x in the pre-state of sign, so that it must have been split > beforehand in order to consider both cases separately: adding an > assert in main will do the trick (see attached file). Admittedly, the > disjunction in requires should also work, but this is not done yet. Thanks for the detailed explanation. The situation is clear for me now. Best regards, david -- David MENTR? - Research engineer, Ph.D. Formal Methods and tools MITSUBISHI ELECTRIC R&D Centre Europe (MERCE) Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59 http://www.fr.mitsubishielectric-rce.eu