Linux and floating-point: nearly there
By pascal on Wednesday, September 14 2011, 19:03 - Permalink
In the process of implementing the value analysis built-ins
Frama_C_precise_cos() from last post, I stumbled on some interesting floating-point results. The sensationalistic title blames Linux, but I didn't fully investigate the problem yet, and it could be somewhere else.
If you have the Frama-C sources lying around, you might be able to reproduce it as below. Otherwise, just read on; it is rather obvious what is wrong, even for a floating-point issue.
$ make bin/toplevel.top ... $ bin/toplevel.top Objective Caml version 3.12.1 # open Ival ;; # set_round_upward () ;; - : unit = () # sin (-3.0) ;; - : float = -2.75991758268585219 # set_round_nearest_even () ;; - : unit = () # sin (-3.0) ;; - : float = -0.141120008059867214
2.76 is a large amplitude for the sine of any angle, and
3.0 isn't even unreasonable as an argument to pass to trigonometric functions. Trigonometric functions on my other OS work from OCaml in all rounding modes. On this Linux computer, the result is reasonable in the default nearest-even mode. This all rather points to an issue in libraries rather than OCaml itself.
If even desktop computers and servers provide this kind of third-rate trigonometric functions, what should we assume about embedded code?