Tag Archives: position

Safe donut
Pascal Cuoq on 16 September 2011

This post documents the steps I followed in order to finish verifying function compute(), picking up from there. Previously on this blog In last episode we had found that some sub-cubes in the search space appeared to lead to dangerous value sets for variable N. These sets were: N ∈...

Read More

Frama-C description
Pascal Cuoq on 14 September 2011

A webpage hosted on 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

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

We have a Csmith-proof framework
Pascal Cuoq on 30 July 2011

Csmith that I mentioned earlier in this blog is a random generator of C programs. That much sounds easy but it generates only well-defined programs which two or more compilers have no excuse for compiling into executables that produce different results. And it generates varied and interesting enough C programs...

Read More

Clang Static Analyzer
Pascal Cuoq on 17 June 2011

From the Clang Static Analyzer homepage: Please help us in this endeavor by reporting false positives. Please help us make Frama-C better by reporting false negatives.

Read More