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