But wait! There may be more!

My colleague Boris Yakobowski is on holidays, and while leisurely browsing the internet, he seems to have stumbled upon my previous post. He e-mailed me about it.

For some reason, it does not feel right to provide much biography when mentioning facetious colleagues perhaps because it would look too self-congratulatory from the outside. Just this once a little bit of context appears to be necessary: Boris is the person who has using Frama-C's value analysis managed to analyze the largest codebase to date. Without qualification this does not mean much: anyone can type "frama-c -val *.c" in a directory and call it an analysis. But there is a point at which one can convincingly argue that the analysis is meaningful and that the results obtained are the best the tool can give. The latter for instance means all remaining alarms have been examined and for each the verifier has some confidence that it is false and an explanation why the analyzer emits the alarm instead of doing the precise thing and not emitting it. In short Boris has reached this point for a pretty big piece of embedded software.

Boris who knows everything about false alarms and generally Frama-C's value analysis' limitations claims that the example from the last post is too simple and suspects me to have doctored it to make it analyze optimally in “only” 7 minutes. How unfair!

The example in last post comes straight from Omar Chebaro's PhD thesis. Omar worked during his PhD on SANTE (more information here) a Frama-C plug-in that combines results from the value analysis plug-in and concolic test-case generation with PathCrawler for one identifying false alarms when possible and two providing input vectors for true alarms (again when possible). There is no reason to doubt Omar's scientific integrity but even if he had a slight bias the bias would not necessarily be to make things easy for the value analysis. He might just as well be tempted to make the value analysis emit more alarms in order to show the necessity of sorting them out with dynamic analysis.

I do have a bias and my motive in last post is clearly to show that the value analysis on that example with the right options can limit its list of alarms to a single one which happens to be a true alarm. But I did not choose the example nor did I modify it to make it easier to analyze.

Note that SANTE is still useful in conditions where the value analysis emits a single alarm: at the end of last post we only know that the alarm is true because of a comment in the source code telling us so. Using PathCrawler to classify that alarm gives SANTE a chance to confirm that it is true and to provide an input vector that the developer would certainly appreciate if only for debugging purposes.