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?

Thanks for the quick response and the information!

Seems like these rounding modes were available in jessie (because I saw
many articles/tutorials about jessie using these floating-point features),
which however is nowhere to be found in the most recent frama-c. Is WP
supposed to be supersede jessie, or am I missing something?

I was wondering what exactly "-wp-model float" does. The ACSL
implementation states that in the float mode "floating-point operations are
defined to be the mathematical ones with a rounding operation." Does that
mean that WP will be fully mimicking the IEEE floating-point standard? So
if in a C program we have "return (x+y)/2", assuming both x and y are
float, then "\result" in the annotation would be as if it was calculated
according the IEEE standard, rather than in real mathematics? If this is
the case, which rounding model will WP use? "\NearestEven" is for
floating-point operations in the annotation, not for operations in the C
program right?


Regards,
Yuhao

On Fri, Jul 8, 2016 at 2:47 AM, Loïc Correnson <loic.correnson at cea.fr>
wrote:

> Hi,
> Support for floats is very experimental and partially implemented in WP.
> You shall at least use -wp-model float, and please, don’t mix it with
> -wp-rte (use Value instead).
>
> Thanks for reporting the bug on \NearestEven. You can workaround the
> problem by overriding
> the standard driver for WP (see /usr/local/share/frama-c/wp/wp.driver), as
> follows :
>
> $ cat fp.driver
> library cfloat:
> ctor "\\NearestAway"()   = "NearestTiesToAway";
> ctor "\\NearestEven"()   = "NearestTiesToEven";
>
> Then:
>
> $ frama-c -wp fp.i -wp-model float -wp-driver fp.driver -wp-print
> [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no
> preprocessing)
> [kernel] Parsing fp.i (no preprocessing)
> fp.i:8:[kernel] warning: Calling undeclared function abs. Old style K&R
> code?
> fp.i:7:[kernel] warning: Neither code nor specification for function abs,
> generating default assigns from the prototype
> [wp] warning: Missing RTE guards
> [wp] 1 goal scheduled
> [wp] [Alt-Ergo] Goal typed_float_fp_average_post : Unknown (Qed:3ms)
> (377ms)
> [wp] Proved goals:    0 / 1
>      Alt-Ergo:        0  (unknown: 1)
> ------------------------------------------------------------
>   Function average
> ------------------------------------------------------------
>
> Goal Post-condition (file fp.i, line 4) in 'average':
> Assume {
>   Type: is_float64(C) /\ is_float64(average_0) /\ is_float64(x) /\
>       is_float64(y) /\ is_sint32(abs_0).
>   (* Pre-condition *)
>   Have: (C <= .1p970) /\ (.1p-967 <= C).
>   If C <= to_float64(real_of_int(abs_0))
>   Then {
>     Have: add_float64(div_float64(x, .1p1), div_float64(y, .1p1)) =
> average_0.
>   }
>   Else { Have: div_float64(add_float64(x, y), .1p1) = average_0. }
> }
> Prove: round_double(NearestTiesToEven, (x + y) / 2) = average_0.
> Prover Alt-Ergo returns Unknown (Qed:3ms) (377ms)
>
> ------------------------------------------------------------
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160708/25859c2d/attachment.html>