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: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Thu, 5 Sep 2013 13:11:27 +0200
- In-reply-to: <52282C81.60306@fr.merce.mee.com>
- References: <5225E3BB.8010903@fr.merce.mee.com> <52275A59.4090701@inria.fr> <52282C81.60306@fr.merce.mee.com>
Hello David, 2013/9/5 David MENTRE <d.mentre at fr.merce.mee.com>: > > [1] Attached program is proved by WP but not by Value analysis with -slevel > 10. I tried adding a "require x >= 0 || x < 0;" or "assert x >= 0 || x < 0;" > to split the state space without success. Any idea on how to prove that with > Value analysis? > 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. Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: q8_if_the_else.c Type: text/x-csrc Taille: 315 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130905/4d866674/attachment.c>
- Follow-Ups:
- [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
- 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
- Prev by Date: [Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic
- Next by Date: [Frama-c-discuss] Introductory slides on Frama-C
- Previous by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Next by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Index(es):