Invalid assertion for overflow check Frama-C

Question

While checking the overflow for short and char data type for add operation, the assertions inserted by Frama-C are seems to be incorrect:

For char and short data the maximum positive and negative values are of integer data type.

What could be the reason for this?

Answer 1

Integral types of rank less than int are converted to either int or unsigned when used in an arithmetic operation (see C11 6.3.1.8 Usual arithmetic conversions). This is why you see the cast to (int) for x and y. Note that by default -rte will not emit warning for downcasts, as they are not undefined behavior (6.3.1.3§3 indicates that signed downcasts are implementation defined and that an implementation may raise a signal). If you add the option -warn-signed-downcast, you'll see the assertions you were probably looking for, which are due to the cast into (char) of the result:

/*@ assert rte: signed_downcast: (int)x+(int)y ≤ 127; */
/*@ assert rte: signed_downcast: -128 ≤ (int)x+(int)y; */

Note that if you store the result into an int, as in

void main(void) {
    char x;
    char y;
    int z;
    x = 1;
    y = 127;
    z = x + y;
    return;
}

There won't be any downcast warning (but the signed overflow warnings will be present).