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