Frama-C Frama-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 MoreSo it may seem that I have a pretty good job for having nothing more important to worry about —that may or may not be accurate— but I worry about the state of the Frama-C documentation in general and of the value analysis in particular. I hate noticing that it's...
Read More