Frama-C The 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 MorePerry E. Metzger takes a look at formal verification [removed dead link]. This is good stuff; there is a lot to agree with here. However agreeing with Perry's post alone would not make a very interesting counterpoint. If agreeing was the only thing I intended to do I might even...
Read More