Browse thread
float rounding
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | David Monniaux <David.Monniaux@e...> |
| Subject: | Re: [Caml-list] float rounding |
In the Astrée project, we use some small C functions and OCaml wrappers to change rounding modes. It's not easy (some systems have fpgetround/fpsetround, others fegetround/fesetround, some have none and you have to use assembly, and old versions of GNU libc on IA32 have fegetround/fesetround that change rounding for the 387 FPU but not for SSE, which may break some external C libraries). [ Hey, we should publish our libraries. ] In addition, some C libraries don't work properly when rounding is not "round to nearest". I filed bugs against FreeBSD libc (printf doesn't work properly with some arguments) and GNU libc (pow() does not work properly). Rounding modes other than the default "round to nearest" tend to be largely untested on many systems and libraries, because few people use them. #pragma FENV_ACCESS is not even implemented on gcc; -frounding-math is supposed to signal rounding modes other than round to nearest, but the documentation states that it's not even sure it works... Not that I want to advertise myself too much, but I think you should read http://www.di.ens.fr/~monniaux/biblio/pitfalls_of_floating_point.pdf if you are concerned about interactions between compilers and floating-point.