Blog

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

Only intervals
Pascal Cuoq on 26 August 2011

More often than is good for me, I find someone on the internet saying something to the effect that \Frama-C only does intervals". Sadly I think I see what they mean. they may be of the school of thought that static analysis is abstract interpretation so that although Frama-C is...

Read More