CodeProver does not detect overflow for non-volatile global variables

Hello,

In an attempt to check the following ticket https://ch.mathworks.com/matlabcentral/answers/374199-codeprover-does-not-detect-overflow-underflow-with-unsigned-variables, I have noticed that CodeProver does not detect potential overflow when manipulating global variables which are not volatile. If I add the volatile keyword, CodeProver does raise a warning.

 int8_t a, b, c;
 volatile int8_t d, e, f;

 void test (void){
     a = b-c; // No warning
     d = e-f; // Warning raised
 }

I have tried also by making some computation on these variables somewhere else in the code, but the result is the same.

Is this a confirmed behavior on your side?

Answer 1

[Alexandre De Barros]

Hello,

I cannot reproduce your results: I have overflows for both volatile and non-volatile variables.

Are b and c full-range in your results ?

Alex

[Benjamin Colle]

Thanks for your answer.

Even without values assigned prior to this operation, I get the behaviour. But at first (with int16 variables), I tried with b = -32768 and c = 32767.

[Benjamin Colle]

After investigation, it has been understood and found that:

- Code Prover, when a main is available, initializes variables to 0

- The assignment of values to those variables was done after the call of the function dealing with those variables

Therefore, Code Prover considered 0-value variables, which indeed do not overflow.

Thanks!