Frama-C 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 MoreAn 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 MoreA 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 MoreBruce Schneier is, among other things, the author of the blog Schneier on Security. He is also one of the co-authors of the Skein cryptographic hash function the SHA-3 contestant being verified in Frama-C's value analysis tutorial in the manual and then on this blog. I feel silly introducing him...
Read MoreInitial setting So, I was checking a small demo of the WP plug-in the other day, just before making a presentation of Frama-C to some future fellow user. This was the traditional binary_search verification presented in the Berlin training session in 2010 but using the WP plugin instead of Jessie....
Read More