Frama-C When 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 MoreIf you have seen the basic presentation of the value analysis, you may remember the following function. void abs(int y) { if (y >= 0) { r = y; return; } else { r = -y; return; } } \Why the two ugly return; statements in a function that needs...
Read More