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

[Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?



Hi Frama-c Friends,

The ACSL implementation
<http://frama-c.com/download/acsl-implementation-Aluminium-20160501.pdf>
(Version
1.11 Implementation in Aluminium-20160501) lists \NearestEven as a rounding
mode (page 23). However, it doesn't appear to be still available at
runtime. When I ran the following code:

/*@   requires 0x1p-967 <= C <= 0x1p970;
  @   ensures \result == \round_double(\NearestEven, (x+y)/2) ;
  @ */

double average(double C, double x, double y) {
  if (C <= abs(x))
    return x/2+y/2;
  else
    return (x+y)/2;
}

using the following command: frama-c -wp -wp-rte -wp-prover coq avg.c, I
get: [wp] user error: Builtin \NearestEven not defined. None of the other
rounding modes was available either.

Any suggestions?
Thanks,
Yuhao
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160707/33cfe92a/attachment.html>