--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Lemma from ACSL doc doesn't verify



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