Frama-C memcpy() 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 MoreA previous post in the value analysis thread in this blog contained this digression: Actually, we can also prevent function Update to keep trace of a previous input buffer, thanks to secondary analyses derived from the value analysis. One of them computes the set of locations written to by a...
Read More