Code Prover Assumptions About Variable Ranges From Data Types

If Polyspace^® cannot determine a variable value from the code, it assumes that the variable has a full range of values allowed by its type.

For instance, for a variable of integer type, to determine the minimum and maximum value allowed, Polyspace uses the following criteria:

The C standard specifies that the range of a signed n-bit integer-type variable must be at least [-(2^n-1-1), 2^n-1-1].
The Target processor type that you specify determines the number of bits allocated for a certain type. For more information, see Target processor type (-target).
Polyspace assumes that your target uses the two’s complement representation for signed integers. The software uses this representation to determine the exact range of a variable. In this representation, the range of a signed n-bit integer-type variable is [-2^n-1, 2^n-1-1].

For example, for an i386 processor:

A char variable has 8 bits. The C standard specifies that the range of the char variable must be at least [-127,127].
Using the two’s complement representation, Polyspace assumes that the exact range of the char variable is [-128,127].

To determine the range that Polyspace assumes for a certain type:

Run verification on this code. Replace type with the type name such as int.
```
type getVal(void);
void main() {
		type val = getVal();
}
```
Open your verification results. On the Source pane, place your cursor on val.
The tooltip provides the range that Polyspace assumes for type. Since getVal is not defined, Polyspace assumes that the return value of getVal has full range of values allowed by type.

Related Topics