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