Frama-C We interrupt our regularly scheduled program to link to this post by Jakob Engblom. The post was prompted by the jury's conclusion in a lawsuit over what appears to be an automotive software glitch that the carmaker is liable.
Read MoreBruce 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 More