--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2013 ---
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 |