--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] floating-point examples



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                    |