Overflow mode for signed integer (-signed-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 signed 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.

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 -signed-integer-overflows. See Command-Line Information (Polyspace Code Prover).

Why Use This Option

Use this option to specify whether to check for signed integer overflows and to specify the assumptions the analysis makes following an overflow.

Settings

Default: forbid

forbid

Polyspace flags signed 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.

This behavior conforms to the ANSI C (ISO C++) standard.

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

#include<stdio.h>

int getVal();

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

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

Note that tooltips on operations with signed 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 signed integer overflows. If an operation results in an overflow, Polyspace analyzes the remaining code but wraps the result of the overflow.

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 [-231..2] or [2..231-2] and the value of i wraps around to -231.

#include<stdio.h>

int getVal();

void func1()
{
    int i = 1;
    i = i << 30;
    // i = 230
    i = i * 2;
    // i = -231
    printf("%d", i);
}
void func2()
{

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

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

warn-with-wrap-around

Polyspace flags signed integer overflows. If an operation results in an overflow, Polyspace analyzes the remaining code but wraps the result of the overflow.

In the following code, j has values in the range [1..231-1] before the orange overflow. Polyspace considers that j has even values in the range [-231..2] or [2..231-2] after the overflow.

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

#include<stdio.h>

int getVal();

void func1()
{
    int i = 1;
    i = i << 30;
    // i = 230
    // Result of * operation overflows
    i = i * 2;
    // i = -231
    printf("%d", i);
}
void func2()
{

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

Note that tooltips on operations with signed 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 signed constants are wrapped around. This behavior cannot be changed by using the options. If you want to detect overflows with signed constants, use the Polyspace Bug Finder™ checker Integer constant overflow.

Command-Line Information

Parameter: -signed-integer-overflows

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

Default: forbid

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

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

Version History

Introduced in R2018b