Frama-C 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 MoreA 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 MoreMore 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 MoreCsmith 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 MoreFrom 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