--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on July 2017 ---
Hi, I try to use WP to verify a floating-point program example excerpted from the IJCAR10 paper by Ali Ayad and Claude Marche, listed as follows: /*@ requires \abs(x) <= 1.0; @ ensures \abs(\result - \exp(x)) <= 0x1p-4; */ double my_exp(double x) { /*@ assert \abs(0.9890365552 + 1.130258690*x + @ 0.5540440796*x*x - \exp(x)) <= 0x0.FFFFp-4; */ return 0.9890365552 + 1.130258690*x + 0.5540440796*x*x; } However, WP says that: [wp] warning: Builtin \exp(real) not defined. Is there a way to verify this example with WP? Do I have to use Jessie for this? Thanks, Junkil