--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Introductory slides on Frama-C



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