Azzera filtri
Azzera filtri

CodeProver does not detect overflow/underflow with unsigned variables

5 visualizzazioni (ultimi 30 giorni)
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.
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.
Is this an issue in CodeProver or a missing configuration, please?
Thank you for your answer,
Best regards

Risposta accettata

Alexandre De Barros
Alexandre De Barros il 26 Dic 2017
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).
  2 Commenti
Benjamin Colle
Benjamin Colle il 27 Dic 2017
Thank you for your answer. I'll change the setting and get back to you after.
Benjamin Colle
Benjamin Colle il 8 Gen 2018
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".

Accedi per commentare.

Più risposte (0)

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by