Linux and floating-point: nearly there Pascal Cuoq on 14 September 2011
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...
Read More