Blog

Tag Archives: value

On memcpy (part 2: the OCaml source code approach)
Pascal Cuoq on 31 January 2011

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 More

On memcpy (part 1: the source code approach)
Pascal Cuoq on 27 January 2011

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 More

Verifying numerical precision with Frama-C's value analysis
Pascal Cuoq on 22 January 2011

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

Why don't you verify the entire Internet ?
Pascal Cuoq on 13 January 2011

... 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

Seven errors game
Pascal Cuoq on 11 January 2011

If 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