Frama-C This blog post is a revised version of part of my submission to the ICPC 2011 Industry Challenge. Please go ahead and read the challenge description. I could only paraphrase it without adding anything to it and so I won't. The study was made with the April development version of...
Read MoreThis post follows that post. For cases 2 and 3 in order to get more complete execution traces we again take advantage of Frama_C_dump_each(). Before launching the analysis we insert a call to this primitive right at the end of RoCo_process() so that local variables of that function will be...
Read MoreIn Carbon 20110201 and earlier versions of Frama-C, if you do not use precautions when analyzing a program with switch statements, you get imprecise results. Consider the example program below. main(int argc, char **argv){ switch(argc){ case 1: Frama_C_show_each_no_args(argc); break; case 2: Frama_C_show_each_exactly_2(argc); /* fall through */ case 3: Frama_C_show_each_2_or_3(argc); break;...
Read MoreA previous post in the value analysis thread in this blog contained this digression: Actually, we can also prevent function Update to keep trace of a previous input buffer, thanks to secondary analyses derived from the value analysis. One of them computes the set of locations written to by a...
Read MoreContext This post is a sequel and conclusion to this remark. Example of derived analysis: slicing When writing a Frama-C plug-in to assist in reverse-engineering source code it does not really make sense to expect the user to check the alarms that are emitted by the value analysis. Consider for...
Read More