MATLAB: Does PolySpace 5.1.1 (R2008a) not warn about possible overflows or underflows when global variables are used

nflovflPolyspace Client for C/C++

I have the following C code. When I run a PolySpace verification, the code that is mentioned in the comments is marked green and I don't receive a warning about possible problems.
unsigned int uintGlobalA, uintGlobalB;
int intGlobalC;
int main () {
    // Subtraction marked with a green check, no warning
    // about possible underflow.
    if ((uintGlobalA - uintGlobalB) < uintGlobalC) {
      //...
    }
    // Addition marked with a green check, no warning
    // about possible overflow.
    if ((uintGlobalA + uintGlobalB) < uintGlobalC) {
      //...
    }
}

Best Answer

This behavior is caused by the fact that the ANSI C90 standard specifies that the value of non-initialized global variables equals zero when a main() function is present.
To change this behavior you can use the following Main Generator option as mentioned in the PolySpace Products for C User's Guide:
 -main-generator-writes-variables
Also, in order for the Main Generator to be able to create a new temporary main(), you will need to set the option "Target/Compilation -> Defined preprocessor Macros" (-D) to, for example,
 main=my_main.
This will allow the global variables to be tested with the full range of possible values.
Related Question