--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] a floating-point program example in WP



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