Frama-C Bruce Dawson has written a superb blog post on a Visual C++ compiler bug (now fixed) covering every aspect an essay on compiler bugs should cover. I really like one section that I am going to quote in full: Security In these paranoid days of the NSA subverting every computer...
Read MoreThe OCaml compiler can generate native code for various architectures. One of the few code generation options is named -compact: $ ocamlopt -help Usage: ocamlopt <options> <files> Options are: ... -compact Optimize code size rather than speed ... One of the effects, perhaps the only effect(?), of this option is...
Read MoreInteger overflows in C A previous post on this blog was a reminder that in C signed integer arithmetic overflow is undefined behavior. In contrast the behavior of overflows in conversions from integer type to signed integer type is implementation-defined. The C99 standard allows for an implementation-defined signal to be...
Read MoreA long time ago, John Regehr wrote a blog post about a 3-3 split vote that occurred while he was finding bugs in C compilers through differential testing. John could have included Frama-C's value analysis in his set of C implementations and then the vote would have been 4-3 for...
Read MoreThis demo shows the usage of Aoraï and Value to generate a scenario of a security leak in the driver of a serial port (Linux kernel 2.6). It stems from the Calmos project with LabSoC at TelecomParisTech/Eurecom C source files and the Frama-C script that launches the analysis are available...
Read More