--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on July 2016 ---
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) ------------------------------------------------------------ -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160708/4aa97bf9/attachment.html>