Frama-C If 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 MoreExtending the framework Some time ago, one of our fellow users asked us whether it was possible to extract the control-flow graph (CFG) of C functions from Frama-C. Fact is, although the CFG is computed during the elaboration of the AST, nothing exists currently to present the information to the...
Read More