Frama-C This 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 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 MoreContext A facetious colleague who claims that he should be better writing his thesis but keeps committing Coq and OCaml files on Frama-C's repository, asked me the following question: Is there a function in Frama-C's kernel that can fold[1] a function over all types that appear in a C program?...
Read More