Frama-C In 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 MoreIn this sequel to a previous post about numerical precision and the value analysis we tackle another extremely common implementation technique the linear interpolation table. In an attempt to make things less boring the approximated function this time is a sine and takes as its argument a double representing an...
Read MoreWhen picking up the title for the previous post on function memcpy I anticipated this second part would describe the Frama_C_memcpy built-in function. The subtitle "part 1: the source code approach" seemed a good idea since the first part was about using C source code to tell the analyzer what...
Read Morememcpy() is one of the few functions standardized as part of C itself instead of an additional API. But that's not what makes it interesting from a static analysis point of view. I think what makes it interesting is that it is used often, and often for tasks that can...
Read More