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] floating-point examples

Claude & Virgile:
Thanks for the pointers.  Looking at the examples, it seems that most (but not all) non-trivial verifications of floating-point examples require Coq and therefore some human intervention (as opposed to being totally automated).  Would this be an accurate generalization of the state of the art at this point in time?
-Steve



On Apr 15, 2013, at 1:19 AM, Claude March? <Claude.Marche at inria.fr> wrote:

> 
> See
> 
> http://toccata.lri.fr/gallery/MyCosineACSL.en.html
> http://hal.inria.fr/hal-00777605
> 
> - Claude
> 
> Le 15/04/2013 04:48, Stephen Siegel a ?crit :
>> I'm looking for some simple, interesting floating-point examples that can be proved with Frama-C+Jessie.  Here is a good example from the ACSL manual:
>> 
>> /*@ requires \abs(\exact(x)) <= 0x1p-5;
>>   @ requires \round_error(x) <= 0x1p-20;
>>   @ ensures \abs(\exact(\result) - \cos(\exact(x))) <= 0x1p-24;
>>   @ ensures \round_error(\result) <= \round_error(x) + 0x3p-24;
>>   @*/
>> float cosine(float x) {
>>   return 1.0f - x * x * 0.5f;
>> }
>> 
>> However, I can't get any of the theorem provers (CVC3, Z3, Alt-Ergo, Gappa, Simplify) to prove either of the generated VCs.  (For all I know, the function may not even satisfy the contract.)  Does anyone know of any examples similar to this that can be proved, or have ideas on how to handle this example?
>> Thanks in advance!
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>> 
> 
> -- 
> 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                    |
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss