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

Задайте, переносится ли результат переполнения или усеченный

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

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

Установите опцию

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

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

Почему использование эта опция

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

Настройки

Значение по умолчанию: allow

forbid

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

  • Красный, Polyspace не анализирует остающийся код в текущем осциллографе.

  • Оранжевый, 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);
    }
}

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);
    }
}

warn-with-wrap-around

Polyspace отмечает переполнение беззнаковых целых чисел. Если операция приводит к переполнению, Polyspace анализирует остающийся код, но переносит результат переполнения. Например, MAX_INT + 1 переносится к MIN_INT.

В следующем коде, 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);
    }
}

Советы

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

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

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

Параметр: -unsigned-integer-overflows
Значение: forbid | allow | warn-with-wrap-around
Значение по умолчанию: allow
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - целочисленное переполнение без знака позволяет
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - целочисленное переполнение без знака позволяет

Введенный в R2018b