Linux and floating-point: nearly there

In the process of implementing the value analysis built-ins Frama_C_precise_sin() and 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?