Frama-C Semi-serious musings During the Frama-C random testing experiment described at length on this blog and this page we found a few bugs in Csmith too. John Regehr one of the Csmith developers and not entirely coincidentally a co-author of the article linked in the previous post is also a co-author...
Read MoreMy presentation Friday at the U3CAT meeting was on the topic of Frama-C Csmith testing. Several posts in this blog already describe facets of this work (it has its own tag). Yet another angle can be found in this short article draft. Said draft by the way will soon need...
Read MoreCsmith 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 MoreHere is a quick recipe for completely wasting a Friday evening: use Csmith to generate a program that GCC happens to mis-compile in 32-bit into an executable that produces the same result as the correct 64-bit compilation of the same program; mess up the Clang double-check by forgetting the -m32...
Read MoreThere won't be many changes in the value analysis' documentation in Nitrogen. For lack of time, the new options, some of which were alluded to in this blog, will remain in their \to be documented" state. But documenting them more fully can always be done here too once they are...
Read More