Overflow mode for unsigned integer (-unsigned-integer-overflows)

Specify whether result of overflow is wrapped around or truncated

Description

This option affects a Code Prover analysis only.

Specify whether Polyspace^® flags unsigned integer overflows and whether the analysis wraps the result of an overflow or restricts it to its extremum value.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node under Code Prover Verification.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors > Check Behavior node.

Command line and options file: Use the option -unsigned-integer-overflows. See Command-Line Information (Polyspace Code Prover).

Why Use This Option

Use this option to specify how Polyspace Code Prover™ reacts to unsigned integer overflows. You can choose to flag an unsigned integer overflow and treat the code following this issue as compromised. Alternatively, you might choose to allow unsigned integer overflows. Depending on the value of this option, Polyspace makes different assumptions when analyzing the code that comes after an unsigned overflow.

Settings

Default: allow

forbid

Polyspace flags unsigned integer overflows. If the Overflow check on an operation is:

• Red, Polyspace does not analyze the remaining code in the current scope.

• Orange, Polyspace analyzes the remaining code in the current scope. Polyspace considers that:

  • After a positive Overflow, the result of the operation has an upper bound. This upper bound is the maximum value allowed by the type of the result.

  • After a negative Overflow, the result of the operation has a lower bound. This lower bound is the minimum value allowed by the type of the result.

In the following code, j has values in the range [1..232-1] before the orange overflow. Polyspace considers that j has even values in the range [2 .. 4294967294] after the overflow. Polyspace does not analyze the printf() statement after the red overflow.

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // Result of * operation overflows
    i = i * 2;
    // Remaining code in current scope not analyzed
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        // Result of * operation may overflow
        j = j * 2;
        // Range of j: even values in [2 .. 4294967294]
        printf("%u", j);
    }
}

Note that tooltips on operations with unsigned integers show (result is truncated) to indicate the analysis mode. The message appears even if the Overflow check is green.

allow

Polyspace does not flag unsigned integer overflows. If an operation results in an overflow, Polyspace analyzes the remaining code but wraps the result of the overflow. For instance, MAX_INT + 1 wraps to MIN_INT. This behavior conforms to the ANSI C (ISO C++) standard.

In this code, the analysis does not flag any overflow in the code. However, the range of j wraps around to even values in the range [0..232-2]] and the value of i wraps around to 0.

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // i = 231
    i = i * 2;
    // i = 0
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        j = j * 2;
        // Range of j: even values in [0 .. 4294967294]
        printf("%u", j);
    }
}

Note that tooltips on operations with unsigned integers show (result is wrapped) to indicate the analysis mode. The message appears even if the analysis does not flag unsigned integer overflows.

warn-with-wrap-around

Polyspace flags unsigned integer overflows. If an operation results in an overflow, Polyspace analyzes the remaining code but wraps the result of the overflow. For instance, INT_MAX + 1 wraps to 0.

In the following code, j has values in the range [1..232-1] before the orange overflow. Polyspace considers that j has even values in the range [0 .. 4294967294] after the overflow.

Similarly, i has value 231 before the red overflow and value 0 after it.

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // i = 231
    i = i * 2;
    // i = 0
    printf("%u", i);
}
void func2()
{

    unsigned int j = getVal();
    if (j > 0) {
        // Range of j: [1..232-1]
        j = j * 2;
        // Range of j: even values in [0 .. 4294967294]
        printf("%u", j);
    }
}

Note that tooltips on operations with unsigned integers show (result is wrapped) to indicate the analysis mode. The message appears even if the Overflow check is green.

In wrap-around mode, an overflowing value propagates and can lead to a similar overflow several lines later. By default, Code Prover shows only the first of similar overflows. To see all overflows, use the option -show-similar-overflows (Polyspace Code Prover).

Tips

• To check for overflows on conversions from unsigned to signed integers of the same size, set Overflow mode for unsigned integer to forbid or warn-with-wrap-around. If you allow unsigned integer overflows, Polyspace does not flag overflows on conversions and wraps the result of an overflow, even if you check for signed integer overflows.

• In Polyspace Code Prover, overflowing unsigned constants are wrapped around. This behavior cannot be changed by using the options. If you want to detect overflows with unsigned constants, use the Polyspace Bug Finder™ checker Unsigned integer constant overflow.

• Code Prover does not show an overflow on bitwise operations on unsigned variables or sbit-s, for instance, in this example:

  volatile unsigned char Y;
  Y = ~Y;

  The verification considers that such bitwise operations are deliberate on your part and you intend an automatic wrap-around in case the result of the operation overflows.

Command-Line Information

Parameter: -unsigned-integer-overflows

Value: forbid | allow | warn-with-wrap-around

Default: allow

Example (Code Prover): polyspace-code-prover -sources file_name -unsigned-integer-overflows allow

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -unsigned-integer-overflows allow

Version History

Introduced in R2018b