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] 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