Frama-C Do you remember the Skein tutorial? It went off to a good start (it started this blog) and then was never really completed. I blame laziness. Looking back at that first post, I notice that indeed, before Boron, we were shipping software without documentation (just think! Ahem). At the time,...
Read MoreSome time back, I reported a Csmith bug against the last git version. This is in no way a rant against Csmith a fine piece of engineering. Csmith does something that I would not have thought possible if you had asked me before I saw it: it generates random C...
Read MoreI have recently added an article \Test driving static analysis tools in search of C code vulnerabilities" by George Chatzieleftheriou and Panagiotis Katsaros on the wiki page of publications relevant to Frama-C. This article benchmarks a number of static analysis tools that it tests for precision (warning about real issues...
Read MoreI should have said this earlier — others might have wanted to join in the fun — but I will be sending an entry to participate in the International Conference on Program Comprehension's Industrial Challenge. My write-up will appear here shortly after the submission deadline.
Read MoreI wish researchers would stop calling the plug-in they are using \Frama-C". "Frama-C" is the framework. It has very few of the properties that are attributed to it. One plug-in or the other usually is to blame or praise. This is not just because when researchers bring it up it...
Read More