Tag Archives: floating-point

Exact case management in floating-point library functions
Pascal Cuoq on 5 August 2013

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...

Read More

The word “binade” now has its Wikipedia page…
Pascal Cuoq on 19 July 2013

… but that's only because I created it. If you are more familiar than me with Wikipedia etiquette feel free to adjust edit or delete this page. Also although a Wikipedia account is necessary to create a page I think it is not required for editing so you can add...

Read More

More on the precise analysis of C programs for FLT_EVAL_METHOD==2
Pascal Cuoq on 15 July 2013

Introduction It started innocently enough. My colleagues were talking of supporting target compilers with excess floating-point precision. We saw that if analyzing programs destined to be compiled with strict IEEE 754 compilers was a lovely Spring day at the beach analyzing for compilers that allow excess precision was Normandy in...

Read More

On the precise analysis of C programs for FLT_EVAL_METHOD==2
Pascal Cuoq on 6 July 2013

There has been talk recently amongst my colleagues of Frama-C-wide support for compilation platforms that define FLT_EVAL_METHOD as 2. Remember that this compiler-set value, introduced in C99, means that all floating-point computations in the C program are made with long double precision, even if the type of the expressions they...

Read More