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] Ergo and problem with integer type

nam nam wrote:
> When I do simple test:
>
> /*@ensures
>   @ \result == (a+b+c);
>   @*/
>
> float triangle(float a, float b, float c){
>     float t ;
>     t = a+b+c;
>     return t;
> }
>
> using Frama C and Ergo the result is ok. 
Yes, because by default the Jessie plugin interprets float calculations 
on mathematical real numbers, hence the ensures is obviously true.

You can turn on the interpretation into floats by

# pragma JessieFloatModel(strict)

In a future version of Jessie, it might become the default.
> But when I try to modify it a
> little:
>
> /*@ensures
>   @ \result == (a+b+c);
>   @*/
>
> int triangle(int a, int b, int c){
>     int t ;
>     t = a+b+c;
>     return t;
> }
>
> the result is so different valid:20% and unknown 80%.
>   
Yes because the default for int type is to interpret into machine 
integers, the additional VCs are to check that no overflow occur.
Here there is no way to guarantee absence of overflow.

And in case of overflow, the ensures clause might be wrong, because + in 
annotations means addition of mathematical,i.e. unbounded, integers.

For example, if int are 32bits, then triangle(maxint,maxint,maxint) 
returns (2^31 - 3) and not (3.2^31 - 3)

If you don't want to bother with overflows, you can ask for 
interpretation into mathematical integers by

# pragma JessieIntegerModel(math)

> I am using jessie 2.19 and ergo 0.9. Did I do something wrong?
> By the way, is there any difference between grammar for pre & post condition
> of WHY and FRAMA C?
>   
If you mean Caduceus and Frama-C: yes there are very close, but there 
are some differences...

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