Frama-C Previously on this blog Although it was so brief that you may have missed it, I previously mentioned here the 2012 RERS Grey Box Challenge an interesting competition where the questions involve programs in C syntax. I pointed out that some questions were about the reachability of assertions in the...
Read MoreIf you liked my earlier proposal for a finer-grained restrict (1 2 3 4) you might like this slightly more serious proposal for named constants in C on Jens Gustedt's blog. Or not. Here is a simple test to tell if you are likely to be interested: if you can...
Read MoreThis post is a follow up of this one A facetious colleague pointed out to me that the print_stmt function that is used to display the CFG in the post mentioned above behaves incorrectly when used over code that include string constants such as the one below: void f(const char...
Read MoreA context-sensitive analysis Frama-C's value analysis is context-sensitive. This means that when a function f2() is called from a caller f1() function f2() is analyzed as many times as the analyzer goes over f1(). Function f2() is analyzed each time with a different program state—the program state corresponding to the...
Read MoreIn a recent post I showed how to use Frama-C's value analysis to prove a particular liveness property true or false of a particular C program. My colleague Sébastien Bardin reliably informs me that the ideas for reducing a liveness property to a reachability property were all in the article...
Read More