Big round number Pascal Cuoq on 15 September 2011
The last post was the 64th in this blog. I just thought you should know that.
Read MoreBlog
Frama-C description Pascal Cuoq on 14 September 2011
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 MoreLinux and floating-point: nearly there Pascal Cuoq on 14 September 2011
In 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 MoreBetter is the enemy of good... sometimes Pascal Cuoq on 12 September 2011
This 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 MoreFun with constants Pascal Cuoq on 9 September 2011
Another 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 More