Blog
Debugging Pascal Cuoq on 26 November 2012
A remark I have not heard about the last two posts is the following. Pascal, how can you, in your last post claim that formal verification would have found the bug in your decimal-to-floating-point function? This is the kind of outrageous claim you rant against in your penultimate post! Formal...
Read MoreFunny floating-point bugs in Frama-C Oxygen's front-end Pascal Cuoq on 19 November 2012
In a previous post almost exactly one year ago before Frama-C Oxygen was released I mentioned that the then future release would incorporate a custom decimal-to-binary floating-point conversion function. The reason was that the system's strtof() and strtod() functions could not be trusted. This custom conversion function is written in...
Read MoreAbout the rounding error in these Patriot missiles Pascal Cuoq on 18 November 2012
An old rant: misusing Ariane 5 in motivation slides I was lucky to be an intern and then a PhD student at INRIA, while it was still called “INRIA” (it is now called “Inria”). This was about when researchers at INRIA and elsewhere were taken to task to understand the...
Read MoreCompiler-driven language development Pascal Cuoq on 17 November 2012
A quiz What is pressing “return” next below going to reveal GCC has done wrong? $ cat t.c #include <limits.h> int x = -1; int main(int c, char **v) { x = INT_MIN % x; return x; } ~ $ gcc -std=c99 t.c ~ $ ./a.out Answer: $ ./a.out Floating...
Read More