Frama-C Here is a little quiz you can use to test your C floating-point expertise. I have tried to write the examples below so that the results do not depend too much on the platform and compiler. This is theoretically impossible since C99 does not mandate IEEE 754 floating-point semantics, but...
Read MoreExploring unfamiliar code Sometimes, one finds oneself in the situation of exploring unfamiliar code. In these circumstances, it is sometimes useful to know which functions a function f() uses. This sounds like something that can be computed from the callgraph, and there exists plenty of tools out there that can...
Read MoreFor printing the results of automated Frama-C tests, we need printing functions with the following properties: they should print all the information available (doing otherwise might mask an existing bug); they should produce results readable enough for a person to validate the result of each test once; and their output...
Read MoreAnswering 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 More