Frama-C A webpage hosted on fedoraproject.org describes Frama-C as follows. I'm quoting the paragraph entirely although it is copyrighted by Red Hat Inc. and others. If I'm not too lazy I will criticize thoroughly which will make this fair use. frama-c is a C source code analysis tool which may be...
Read MoreIn the process of implementing the value analysis built-ins Frama_C_precise_sin() and Frama_C_precise_cos() from last post I stumbled on some interesting floating-point results. The sensationalistic title blames Linux but I didn't fully investigate the problem yet and it could be somewhere else. If you have the Frama-C sources lying around you...
Read MoreThis post is about widening. This technique was shown in the second part of a previous post about memcpy() where it was laboriously used to analyze imprecisely function memcpy() as it is usually written. The value analysis in Frama-C has the ability to summarize loops in less time than they...
Read MoreAnother facetious colleague reports a strange behavior with the following C program: int main (void) { int x = 100; int y = 042; int z = 005; printf (\%d" x+y+z); return (x+y+z) - 147; }
Read MoreSafe C interpreters galore The last release of CompCert includes a safe C interpreter based on the compiler's reference semantics. Like KCC and Frama-C's value analysis it detects a large class of undefined behaviors and some unspecified ones. Like them in order to remain useful it needs to make some...
Read More