--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on December 2009 ---
Hollas Boris (CR/AEY1) wrote: > More precisely, consider this code: > > > //@ lemma mean_property2: \forall integer l, h; l <= h ==> l <= (l+h)/2 <= h; > > //@ ensures l <= \result <= h; > Int foo(int l, int h) { > return (l+h)/2; > } > > Main() { > int a = foo(maxint, maxint); > } > > > I can't test this with my installation because Beryllium1 doesn't verify mean_property2. If this lemma can be proved however, what result is Jessie supposed to give on this code? > Please install Alt-Ergo 0.9. Here is the screenshot I got from a slightly modified version of your code (two more lemmas). 1) Lemmas are shown valid by Alt-Ergo but not by other provers 2) arith overflow check on (l+h) fails for all provers: this is expected of course 3) post-conditions do not hold, expected two. 4) the rest is proved by most provers (Simplify is not good with large int constants...) This explains why I said that SMT provers do not know about division. But giving a few lemmas helps them properly. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex | -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: hollas3.c Type: text/x-csrc Taille: 340 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091203/6e266990/attachment-0001.c -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: hollas3.png Type: image/png Taille: 74243 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091203/6e266990/attachment-0001.png