Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
  • From: yzhu at utexas.edu (Yuhao Zhu)
  • Date: Thu, 7 Jul 2016 18:33:55 -0500
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>