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

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



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