Blog

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 More

Linux 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 More

Better 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 More

Fun 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

CompCert gets a safe interpreter mode
Pascal Cuoq on 29 August 2011

Safe 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