--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on September 2013 ---
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>