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] Jessie plugin


Le 09/05/2012 08:35, Boris Hollas a ?crit :
> On Mon, 2012-05-07 at 20:31 +0200, Claude Marche wrote:
>> /*@ requires \valid(AB_Ptr)&&  \valid(CD_Ptr);
>>      @ behavior zero:
>>      @ assumes \exact(*AB_Ptr)>  \exact(*CD_Ptr) ;
>>      @ ensures  result == 1
>>      @ behavior one:
>>      @ assumes \exact(*AB_Ptr)<= \exact(*CD_Ptr);
>>      @ ensures  result == 0;
>>      @ */
>
> I have a related question. Is \exact(x), when used in a precondition,
> equivalent to x (if x is a parameter of the function)?

No it isn't. On the contrary, there is no contraint at all between them. 
So when using \exact you typically need to put as precondition something 
like \abs(\round_error(x)) <= some constant

> The example in
> the ACSL documention suggests it isn't.

Indeed.

> Are Coq or Gappa required to use \exact and is user interaction
> necessary to prove VCs?

No and no. Indeed, if one uses the pragma JessieFloatModel(math) then 
Gappa is typically not needed, and regarding computation on real 
numbers, some automated provers perform quite well (CVC3, Z3, and 
sometimes Alt-Ergo). Coq is just an alternative in case the math is too 
complex for automated provers.

Gappa is typically useful to prove something about rounding errors.

A few examples of C programs with floats, specified with ACSL and proved 
with the Jessie-plugin are available at the URLs:

http://proval.lri.fr/gallery/fp.en.html

http://hisseo.saclay.inria.fr/gallery.html

http://www.lri.fr/~sboldo/research.html


Hope this helps,

- Claude


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |