Frama-C Introduction This post introduces a new series about the art of helping the value analysis to be more precise. Until now, in the numerical precision series of this blog, this was easy enough. There was a single input variable and the obvious way to get more precise output values was...
Read MoreThis sort of question (here about the trade-offs involved in the choice of the level of intermediate language to statically analyze) is the reason I still visit StackOverflow despite everything that is wrong with it.
Read MoreThis post follows that post where a typical double-precision implementation for a cosine function is shown. That implementation is not a correctly rounded implementation but its double result is precise to a level close to what the double-precision floating-point representation allows. It uses low-level tricks that make it faster on...
Read MoreI once claimed in a comment that with the value analysis, when the source code is fully available, you can analyze many executable C programs with maximum precision. For this to work, all inputs must have been decided in advance and be provided. It can therefore be likened to running...
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 More