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

Укажите, обернут ли результат переполнения вокруг или усечен

Описание

Эта опция влияет только на анализ Code Prover.

Задайте, является ли Polyspace® флаги беззнаковые целочисленные переполнения и то, переносит ли анализ результат переполнения или ограничивает его значением extremum.

Задать опцию

Пользовательский интерфейс (только для продуктов): На панели Configuration опция находится на узле Check Behavior под Code Prover Verification.

Командная строка и файл опций: Используйте опцию -unsigned-integer-overflows. См. «Информация о командной строке».

Зачем использовать эту опцию

Используйте эту опцию, чтобы задать, проверять ли на беззнаковые целочисленные переполнения и задать допущения, которые делает анализ после переполнения.

Настройки

По умолчанию: allow

forbid

Polyspace помечает беззнаковые целочисленные переполнения. Если проверка Overflow для операции:

  • Красный, Polyspace не анализирует оставшийся код в текущих возможностях.

  • Orange, Polyspace анализирует оставшийся код в текущих возможностях. Polyspace считает, что:

    • После положительного Overflow результат операции имеет верхнюю границу. Эта верхняя граница является максимальным значением, разрешенным типом результата.

    • После отрицательного Overflow результат операции имеет нижнюю границу. Эта нижняя граница является минимальным значением, разрешенным типом результата.

В следующем коде j имеет значения в область значений [1.. 232-1] перед оранжевым переполнением. Polyspace считает, что j имеет четные значения в области значений   [2 .. 4294967294] после переполнения. Polyspace не анализирует printf() оператор после красного переполнения.

#include<stdio.h>

unsigned int getVal();

void func1()
{
    unsigned int i = 1;
    i = i << 31;
    // Result of * operation overflows
    i = i * 2;
    // Remaing 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);
    }
}

Обратите внимание, что подсказки к операциям с беззнаковыми целыми числами показывают (result is truncated) для указания режима анализа. Сообщение появляется, даже если Overflow проверка зеленого цвета.

allow

Polyspace не помечает беззнаковые целочисленные переполнения. Если операция приводит к переполнению, Polyspace анализирует оставшийся код, но переносит результат переполнения. Для образца, MAX_INT + 1 переносы в MIN_INT. Это поведение соответствует стандарту ANSI C (ISO C++).

В этом коде анализ не помечает никакого переполнения в коде. Однако область значений j Переносы к четным значениям в область значений [0.. 232-2]] и значение i оборачивается к 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);
    }
}

Обратите внимание, что подсказки к операциям с беззнаковыми целыми числами показывают (result is wrapped) для указания режима анализа. Сообщение появляется, даже если анализ не помечает беззнаковые целочисленные переполнения.

warn-with-wrap-around

Polyspace помечает беззнаковые целочисленные переполнения. Если операция приводит к переполнению, Polyspace анализирует оставшийся код, но переносит результат переполнения. Для образца, INT_MAX + 1 переносы в 0.

В следующем коде j имеет значения в область значений [1.. 232-1] перед оранжевым переполнением. Polyspace считает, что j имеет четные значения в области значений  [0 .. 4294967294] после переполнения.

Точно так же i имеет значение 231 перед красным переполнением и значением 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);
    }
}

Обратите внимание, что подсказки к операциям с беззнаковыми целыми числами показывают (result is wrapped) для указания режима анализа. Сообщение появляется, даже если Overflow проверка зеленого цвета.

В режиме обтекания переполненное значение распространяется и может привести к аналогичному переполнению нескольких строк позже. По умолчанию Code Prover показывает только первое из подобных переполнений. Чтобы увидеть все переполнения, используйте опцию -show-similar-overflows.

Совет

  • Чтобы проверить переполнение при преобразованиях из беззнаковых в подписанные целые числа того же размера, установите Overflow mode for unsigned integer равным forbid или warn-with-wrap-around. Если вы разрешаете беззнаковые целочисленные переполнения, Polyspace не помечает переполнения при преобразованиях и переносит результат переполнения, даже если вы проверяете на наличие подписанных целочисленного переполнения.

  • В Polyspace Code Prover™ переполненные неподписанные константы обернуты. Это поведение не может быть изменено при помощи опций. Если вы хотите обнаружить переполнения с помощью неподписанных констант, используйте проверку Polyspace Bug Finder™ Unsigned integer constant overflow.

  • Code Prover не показывает переполнение при побитовых использованиях с беззнаковыми переменных, например, в этом примере:

    volatile unsigned char Y;
    Y = ~Y;
    Верификация считает, что такие побочные операции являются преднамеренными с вашей стороны, и вы планируете автоматическое завершение в случае, если результат операции переполнен.

Информация о командной строке

Параметр: -unsigned-integer-overflows
Значение: forbid | allow | warn-with-wrap-around
По умолчанию: allow
Пример (Code Prover): Polyspace Code Prover -sources file_name -unsigned-integer-overflows позволяют
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -unsigned-integer-overflows позволяют
Введенный в R2018b