From: David Monniaux <David.Monniaux@ens.fr>
To: Olivier Andrieu <oandrieu@nerim.net>
Cc: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>,
caml-list@inria.fr
Subject: Re: [Caml-list] float rounding
Date: Sun, 26 Nov 2006 02:51:52 +0100 [thread overview]
Message-ID: <4568F338.2060307@ens.fr> (raw)
In-Reply-To: <17698.53404.408141.945571@karryall.dnsalias.org>
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.
prev parent reply other threads:[~2006-11-26 1:52 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2006-09-30 18:25 Sean McLaughlin
2006-10-01 12:44 ` [Caml-list] " Florent Monnier
2006-10-01 13:36 ` Gerd Stolpmann
2006-10-01 16:36 ` Xavier Leroy
2006-11-23 23:00 ` David Monniaux
2006-10-03 13:41 ` Christophe Raffalli
2006-10-03 19:59 ` Christophe Raffalli
2006-10-03 21:05 ` Olivier Andrieu
2006-11-26 1:51 ` David Monniaux [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4568F338.2060307@ens.fr \
--to=david.monniaux@ens.fr \
--cc=Christophe.Raffalli@univ-savoie.fr \
--cc=caml-list@inria.fr \
--cc=oandrieu@nerim.net \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox