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: Fri, 8 Jul 2016 08:48:39 -0500
- In-reply-to: <103435E1-2B62-42EE-8D4C-738DB5ADA063@cea.fr>
- References: <CAMr8bK3MyGhV=GdCLUS1JXii-yNNq_7cjHiuJLpq4h6i_KuS2g@mail.gmail.com> <103435E1-2B62-42EE-8D4C-738DB5ADA063@cea.fr>
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>
- References:
- [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
- From: yzhu at utexas.edu (Yuhao Zhu)
- [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
- Prev by Date: [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
- Next by Date: [Frama-c-discuss] JFLA 2017 : premier appel à communications
- Previous by thread: [Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?
- Next by thread: [Frama-c-discuss] JFLA 2017 : premier appel à communications
- Index(es):