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
- Subject: [Frama-c-discuss] Introductory slides on Frama-C
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- Date: Thu, 05 Sep 2013 14:16:20 +0200
- In-reply-to: <CA+yPOVh=E0wzc=wO3ZZLzo06J=Hr7_OEZPbkJanqJKp3kexBKQ@mail.gmail.com>
- References: <5225E3BB.8010903@fr.merce.mee.com> <52275A59.4090701@inria.fr> <52282C81.60306@fr.merce.mee.com> <CA+yPOVh=E0wzc=wO3ZZLzo06J=Hr7_OEZPbkJanqJKp3kexBKQ@mail.gmail.com>
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
- References:
- [Frama-c-discuss] Introductory slides on Frama-C
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Introductory slides on Frama-C
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] Introductory slides on Frama-C
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Introductory slides on Frama-C
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Introductory slides on Frama-C
- Prev by Date: [Frama-c-discuss] Introductory slides on Frama-C
- Next by Date: [Frama-c-discuss] [Jessie] loop invariant
- Previous by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Next by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Index(es):