--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2016 ---
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>