Blog

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

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