CodeProver does not detect overflow/underflow with unsigned variables

Hello,

I have noticed that Code Prover does not raise a warning in case of a subtraction between 2 unsigned variables. It does raise for 2 signed ones, but not with 2 unsigned.

Example

 void test (void){
     uint8_t a, b, c;
     b = foo();
     c = bar();
     a = b-c;
 }

This operation b-c is not seen as a potential overflow/underflow occurence.

Question

Is this an issue in CodeProver or a missing configuration, please?

Thank you for your answer,

Best regards

Answer 1

[Alexandre De Barros]

Hello,

In standard C, there is no overflow on unsigned types. The C99 standard (§6.2.5/9) states:

"A computation involving unsigned operands can never overflow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type."

Hence, by default, Code Prover will not report this kind of overflow.

Now, if you are interested by detecting them, you can change the default behavior thanks to the option "Detect overflows".

In the configuration pane, choose "Code Prover Verification" then "Check Behavior" and on the right page, for the option "Detect Overflows", select "signed and unsigned".

Please note that in your example, the overflow will appear on the assignment to the variable a, since the subtraction is performed on the int type (integral promotion).

Alex

[Benjamin Colle]

Thank you for your answer. I'll change the setting and get back to you after.

[Benjamin Colle]

By adding the parameter -scalar-overflows-checks signed-and-unsigned to the command polyspace-code-prover-nodesktop, it is possible now to detect unsigned "overflows".

Thanks!