-signed-integer-overflows)Укажите, обернут ли результат переполнения вокруг или усечен
Эта опция влияет только на анализ Code Prover.
Задайте, является ли Polyspace® флаги со знаком целочисленного переполнения и то, переносит ли анализ результат переполнения или ограничивает его значением extremum.
Пользовательский интерфейс (только для продуктов): На панели Configuration опция находится на узле Check Behavior под Code Prover Verification.
Командная строка и файл опций: Используйте опцию -signed-integer-overflows. См. «Информация о командной строке» (Polyspace Code Prover).
Используйте эту опцию, чтобы определить, проверять ли целочисленное переполнение со знаком и определить допущения, которые делает анализ после переполнения.
По умолчанию:
forbid
forbid
Флаги Polyspace подписаны целочисленным переполнением. Если проверка Overflow для операции:
Красный, Polyspace не анализирует оставшийся код в текущих возможностях.
Orange, Polyspace анализирует оставшийся код в текущих возможностях. Polyspace считает, что:
После положительного Overflow результат операции имеет верхнюю границу. Эта верхняя граница является максимальным значением, разрешенным типом результата.
После отрицательного Overflow результат операции имеет нижнюю границу. Эта нижняя граница является минимальным значением, разрешенным типом результата.
Это поведение соответствует стандарту ANSI C (ISO C++).
В следующем коде j имеет значения в область значений [1.. 231-1] перед оранжевым переполнением. Polyspace считает, что j имеет четные значения в области значений [2 .. 2147483646] после переполнения. Polyspace не анализирует printf() оператор после красного переполнения.
#include<stdio.h>
int getVal();
void func1()
{
int i = 1;
i = i << 30;
// Result of * operation overflows
i = i * 2;
// Remaing 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);
}
} |
Обратите внимание, что подсказки к операциям со знаковыми целыми числами показывают (result is truncated) для указания режима анализа. Сообщение появляется, даже если Overflow проверка зеленого цвета.
allow
Polyspace не помечает подписанные целочисленное переполнение. Если операция приводит к переполнению, Polyspace анализирует оставшийся код, но переносит результат переполнения.
В этом коде анализ не помечает никакого переполнения в коде. Однако область значений j оборачивается к четным значениям в области значений [-231.. 2] или [2.. 231-2] и значение i оборачивается к -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);
}
} |
Обратите внимание, что подсказки к операциям со знаковыми целыми числами показывают (result is wrapped) для указания режима анализа. Сообщение появляется, даже если анализ в этом режиме не помечает целочисленного переполнения со знаком.
warn-with-wrap-around
Флаги Polyspace подписаны целочисленным переполнением. Если операция приводит к переполнению, Polyspace анализирует оставшийся код, но переносит результат переполнения.
В следующем коде j имеет значения в область значений [1.. 231-1] перед оранжевым переполнением. Polyspace считает, что j имеет четные значения в области значений [-231.. 2] или [2.. 231-2] после переполнения.
Точно так же i имеет значение 230 перед красным переполнением и значением -231 после него.
#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);
}
} |
Обратите внимание, что подсказки к операциям со знаковыми целыми числами показывают (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™ checker Integer constant overflow.
Параметр:
-signed-integer-overflows |
Значение:
forbidallow | warn-with-wrap-around |
По умолчанию:
forbid |
Пример (Code Prover):
Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources |
Overflow mode for unsigned integer (-unsigned-integer-overflows) | -show-similar-overflows (Polyspace Code Prover) | Overflow (Polyspace Code Prover)