Frama-C A prospective user experimenting with Frama-C wonders whether it is possible to verify the behavior of an interrupt-driven system for all possible interlacing of interrupts. We assume, for now, that interrupts are themselves uninterruptible. The prospective user wants to verify that nothing wrong happens when each interrupt is called once,...
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 MoreHere is a series of posts that highlight interesting features in the recently released Frama-C Nitrogen 20111001. There is new functionality in Nitrogen, that we hope will entice both existing and prospective users. Other improvements yet will only have meaning for existing users. I will start off with two items...
Read MorePerhaps you are looking for something to do pending the upcoming release of Frama-C (someone called it \Nitrozen" once by accident in a commit message. I would like the name to stick but I anticipate it won't)… Or you are already a serious user of the value analysis plug-in or...
Read MoreA number of colleagues and I have been tasked with writing a summary of an article they published in 2010. Each of us has to do this for an article of theirs, that is. I chose the article whose long version title is \A Mergeable Interval Map" (link PDF available...
Read More