Re: Using crlibm as the default math library in GCC sources

[Geert Bosch <bosch at adacore dot com>]

On Nov 14, 2007, at 05:27, Vincent Lefevre wrote:

> > Initially, float could simply use double and cast the result.
> > For double->float the results will remain correctly rounded.
>
> Yes, very probably, but this needs to be proven for each supported
> function, due to the double rounding problem (this may take some time
> for functions like pow).

If a real number is rounded to the nearest number in a binary floating
point format with 2*p+1 bits and that result rounded again to
a p-bit float, the result is the same as if the original value was
rounded to a p-bit float directly.

  -Geert

PS. Sorry, dont' have a reference to a proof handy at the moment.