[Frama-c-discuss] Is “\NearestEven” available in frama-c Aluminium-20160501?

Loïc Correnson loic.correnson at cea.fr
Fri Jul 8 09:47:53 CEST 2016

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";


$ 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>

More information about the Frama-c-discuss mailing list