-unsigned-integer-overflows)Укажите, обернут ли результат переполнения вокруг или усечен
Эта опция влияет только на анализ Code Prover.
Задайте, является ли Polyspace® флаги беззнаковые целочисленные переполнения и то, переносит ли анализ результат переполнения или ограничивает его значением extremum.
Пользовательский интерфейс (только для продуктов): На панели Configuration опция находится на узле Check Behavior под Code Prover Verification.
Командная строка и файл опций: Используйте опцию -unsigned-integer-overflows. См. «Информация о командной строке» (Polyspace Code Prover).
Используйте эту опцию, чтобы задать, проверять ли на беззнаковые целочисленные переполнения и задать допущения, которые делает анализ после переполнения.
По умолчанию:
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 (Polyspace Code Prover).
Чтобы проверить переполнение при преобразованиях из беззнаковых в подписанные целые числа того же размера, установите 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 |
Значение:
forbidallow | warn-with-wrap-around |
По умолчанию:
allow |
Пример (Code Prover):
Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources |
Overflow mode for signed integer (-signed-integer-overflows) | -show-similar-overflows (Polyspace Code Prover) | Overflow (Polyspace Code Prover)