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 MoreAs I write these words, Virgile Prevosto, one of the dozen Frama-C developers, has been running 320km (starting last Sunday at 10am CET). He has about 12km left before he finishes the "Tor des Géants" endurance trail. That's TWO HUNDRED FULL-FLEDGED MILES in imperial units and I write this with...
Read MoreThe last post was the 64th in this blog. I just thought you should know that.
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 MoreIn 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