My colleague Bernard Botella pointed out an interesting example in an offline discussion following the last quiz.

## The setup

Consider the snippet:

int s; unsigned u1, u2; ... s = u1 - u2;

The programmer's intention with the assignment is to compute, in variable `s`

of type `int`

, the mathematical difference between the value of `u1`

and the value of `u2`

. You would expect that, using automatic plug-ins in Frama-C, ey would be able to check that the initial values for `u1`

and `u2`

are in ranges for which this is always what happens.

In fact, this looks like a perfect assignment for Rte and the value analysis. Rte can generate assertions for the various conversions and the value analysis can check whether the conditions are satisfied, following the method outlined in a recent post.

This is, after all, exactly what static analyzers — and coding rules that forbid overflows — are for.

## An obvious false positive

The overflow in the subtraction `u1 - u2`

looks like it can be justified away. After all, such a warning is emitted when `u1==3`

and `u2==5`

, and `s`

will still receive the expected value `-2`

after the implementation-defined conversion from the value of expression `u1 - u2`

, that is, `UINT_MAX - 1`

, to `int`

.

The programmer may think “okay, I can see why I get this warning, it happens as soon as `u2`

is larger than `u1`

, but this is defined and, in my case, innocuous. I only want to check that the mathematical difference fits in `s`

. The check about the absence of overflow in the conversion to `int`

is what I am really interested in.”

Say that the programmer is using the Rte plug-in to express the conditions for both the subtraction and the implicit conversion to `int`

to be safe, pretty-printing an annotated program as a result:

$ frama-c -rte-unsigned-ov -rte t.c -print ... void main(void) { /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ /*@ assert rte: u1-u2 ≥ 0; */ s = (int)(u1 - u2); return; }

Since the programmer has seen that the second assertion, about an overflow in the subtraction `u1 - u2`

, is too restrictive, preventing use with `u1==3`

and `u2==5`

, ey removes it.
The programmer instead focuses on making sure that there is no overflow in the conversion to `int`

of the difference, and feels confident if ey sees that there isn't any warning about that. It seems normal, right?

void main(void) { /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ s = (int)(u1 - u2); return; }

## But…

Consider the case where `u1`

is very small, `u2`

is very large, and the value analysis has been able to infer this information relatively precisely. We assume 0 ≤ u1 ≤ 10 and 3000000000 ≤ u2 ≤ 4000000000 for this example:

/*@ requires 0 <= u1 <= 10 ; requires 3000000000 <= u2 <= 4000000000 ; */ void main(void) { /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */ s = (int)(u1 - u2); return; }

In this case, the value analysis does not warn about the conversion to `int`

...

$ frama-c -val -lib-entry u.c ... u.c:8:[value] Assertion got status valid.

... but the value in `s`

is not the mathematical difference between `u1`

and `u2`

.

## Conclusion

The conclusion is that looking at overflows atomically is not a silver bullet. Granted, if all possible overflows in the program are verified to be impossible, then machine integers in the program observationally behave like mathematical integers. But the more common case is that some overflows do in fact happen in the program and are justified as benign by the programmer. The issue pointed out by Bernard Botella is that it is possible to justify an overflow, for which the rule seems too strict, by exhibiting input values for which the expected result is computed, and then to be surprised by the consequences.

Perhaps in another post, we can look at ways around this issue.