2011-09-14-Linux-and-floating-point-nearly-there.html

---
layout: post
author: Pascal Cuoq
date: 2011-09-14 16:03 +0200
categories: floating-point value-builtins
format: xhtml
title: "Linux and floating-point: nearly there"
summary: 
---
{% raw %}
<p>In the process of implementing the value analysis built-ins <code>Frama_C_precise_sin()</code> and <code>Frama_C_precise_cos()</code> from <a href="/index.php?post/2011/09/12/better">last post</a>  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.</p> 
<p>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.</p> 
<pre>$ 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 
</pre> 
<p><code>2.76</code> is a large amplitude for the sine of any angle  and <code>3.0</code> 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.</p> 
<p>If even desktop computers and servers provide this kind of third-rate trigonometric functions  what should we assume about embedded code?</p>
{% endraw %}