--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2017 ---
Hi, There is no definition (yetâ¦) for the ACSL \exp builtin in WP. You shall define a logical function instead, and use axioms and/or WP drivers (see documentation) to feed SMT solvers with suitable properties of exponential⦠L. > Le 31 juil. 2017 à 21:07, Junkil âDavidâ Park <juki14 at gmail.com> a écrit : > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss