Frama-C In 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 MoreFrama-C's value analysis wasn't aimed at verifying numerical precision of C functions when it was conceived. There already was a specialized project for this purpose. However the value analysis needed to handle floating-point computations correctly (that is without omitting any of the possible behaviors the function can have at run-time)...
Read More... or at least the C codebase available on there, anyway? Don't be fooled by the positive examples presented here and there. Verifying arbitrary programs is still arbitrarily difficult. There is some cherry-picking going on in the results we, and others, present. In the case of Frama-C's value analysis, dynamic...
Read More