Blog

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

From Pascal strings to Python tuples
Pascal Cuoq on 31 July 2013

Quiz time What does the program below do? #include <stdio.h> int main(){ struct { int t[4]; int u; } v; v.u = 3; v.t[4] = 4; printf(\v.u=%d" v.u); return 0; } Two answers are “it prints v.u=4” and “it prints v.u=3”: $ gcc t.c && ./a.out v.u=4 $ gcc -O2...

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

Arithmetic overflows in Fluorine
Pascal Cuoq on 9 July 2013

There is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...

Read More