Frama-C 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 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 MoreWhen researchers start claiming that they have a sound and complete analyzer for predicting whether a program statement is reachable, it is time to build a database of interesting programs. Goldbach's conjecture My long-time favorite is a C program that verifies Goldbach's conjecture (actual program left as an exercise to...
Read More