Frama-C Answering the two questions from last post in reverse order: What shorter analysis context would test arbitrarily long sequences of interrupts, with repetitions? There was a hint in the previous post in the link to the Skein-256 tutorial. A stronger hint would have been to link directly to this post...
Read MoreA 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 MoreAccording to David Crocker's blog Escher C Verifier has been released. Congratulations!
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 MoreThis ranty post is because I never tire of trying the content management system on weird characters for its URLs. No, this post is really because David Mitchell himself has a new post up I find interesting. It very much follows the same general direction his posts usually do (if...
Read More