Frama-C This 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 MoreIn a previous post there was a cosine function that I made up for the purpose of blogging about it. Let us now look at a real cosine function (OpenBSD's libm derived from widespread code written at Sun in the 1990s) to get a feeling how far off we were:...
Read More