Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Exact case management in floating-point library functions

The documentation of the correctly-rounded CRlibm floating-point library states, for the difficult pow() function (p. 159):

Directed rounding requires additional work, in particular in subnormal handling and in exact case management. There are more exact cases in directed rounding modes, therefore the performance should also be inferior.

The phrase “exact case” refers to inputs that need to be treated specially because no number of “Ziv iterations”, at increasing precisions, can ever resolve which way the rounding should go.

Quiz: Isn't an exact case an exact case independently of the rounding mode? How can exact cases vary with the rounding mode?

If you can answer the above quiz without having to rubber duck through the entire question on an internet forum, you have me beat.


1. On Monday, August 5 2013, 18:26 by pascal

In my defense, the name “exact case” is a clever bit of mis-direction on the part of the authors of the CRlibm documentation.