MATLAB: What does “generated main writes randomly into each global and extern and static variable” in the documentation for PolySpace R2008a mean

Question

The documentation for the PolySpace option "main-generator-writes-variables" says that the generated main writes randomly into each global and extern and static variable. I would like to know which value is written randomly into the global variables.

Answer 1

When we say that PolySpace initializes global variables to random, it means that PolySpace will consider the global variable could have any values on its type definition. It will not favor one value among others but considers all. This is not a dynamic execution.

For instance, if we have the instruction 'varglobal +1' on a global integer variable varglobal, PolySpace will consider that we could have an overflow if varglobal is MAX_INT and so will put an unproven OVFL check on the +.