Frama-C Csmith as a static analyzer fuzzer A new version of Csmith, the generator of random defined C programs, was released a few days ago. This is the version that many functions in Frama-C Nitrogen were debugged against. Conversely a few bugs in the development versions of Csmith characterized by programs...
Read MoreIt is very easy to make snap judgments about other static analyzers when you are yourself working on one. You do not even need to act in bad faith: you just try the other tools on the programs that you worked hard to give interesting results on — difficult examples,...
Read MoreSpeaking of bug fixes, here is what a proper post-release patch looks like. This patch fixes five issues identified since Nitrogen was released. I have not tested the patch itself (I have not even tried applying it to the original tarball) — this is where you come in dear reader....
Read MoreIn the course of restructuring the value analysis, I noticed a difference in some regression tests. The \after" version had some new warnings that weren't in the "before" version. After further investigation it turned out that displaying the warnings was correct and that the "before" version was unsound. This soundness...
Read MoreIntroduction: of Spivak pronouns In this post, I really let fly the Spivak pronouns. They are not used for the first time in this blog or in documentation but they are abused here. I have no serious justification for this sudden peak. I have a couple of unserious ones: I...
Read More