-signed-integer-overflows)Укажите, будет ли результат переполнения окружен или усечен
Этот параметр влияет только на анализ программы проверки кода.
Укажите, будет ли Polyspace ® помечать целочисленные переполнения со знаком и будет ли анализ переносить результат переполнения или ограничивать его экстремальным значением.
Пользовательский интерфейс (только для настольных ПК): На панели Конфигурация (Configuration) параметр находится в узле Проверка поведения (Check Behavior) в разделе Проверка проверочного кода (Code Prover Verification).
файл командной строки и параметров: Использовать параметр -signed-integer-overflows. См. раздел Сведения о командной строке.
Эта опция используется для определения необходимости проверки переполнения целочисленных значений со знаком и указания допущений, которые делает анализ после переполнения.
По умолчанию:
forbid
forbid
Флаги Polyspace, подписанные целочисленными переполнениями. Если проверка переполнения для операции:
Красный, Polyspace не анализирует оставшийся код в текущей области.
Оранжевый, Polyspace анализирует оставшийся код в текущей области. Полиспейс считает, что:
После положительного переполнения результат операции имеет верхнюю границу. Эта верхняя граница является максимальным значением, допустимым типом результата.
После отрицательного переполнения результат операции имеет нижнюю границу. Эта нижняя граница является минимальным значением, допустимым типом результата.
Это поведение соответствует стандарту ANSI C (ISO C++).
В следующем коде: j имеет значения в диапазоне [1..231-1] перед оранжевым переполнением. Полиспейс считает, что 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) для указания режима анализа. Сообщение появляется, даже если проверка переполнения имеет зеленый цвет.
allow
Polyspace не помечает подписанные целочисленные переполнения. Если операция приводит к переполнению, Polyspace анализирует оставшийся код, но переносит результат переполнения.
В этом коде анализ не помечает переполнение в коде. Однако диапазон j обтекает до четных значений в диапазоне [-231..2] or [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] перед оранжевым переполнением. Полиспейс считает, что j имеет четные значения в диапазоне [-231..2] or [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) для указания режима анализа. Сообщение появляется, даже если проверка переполнения имеет зеленый цвет.
В режиме обхода значение переполнения распространяется и может привести к аналогичному переполнению нескольких строк позже. По умолчанию средство проверки кода показывает только первое из аналогичных переполнений. Для просмотра всех переполнений используйте опцию -show-similar-overflows.
Для проверки переполнения при преобразованиях из неподписанных в подписанные целые числа одного размера установите режим переполнения для неподписанных целых чисел в значение forbid или warn-with-wrap-around. Если разрешены неподписанные целочисленные переполнения, Polyspace не помечает переполнения при преобразованиях и переносит результат переполнения, даже если проверяется наличие подписанных целочисленных переполнений.
В Polyspace Code Prover™ переполняющиеся подписанные константы обтекаются. Это поведение нельзя изменить с помощью параметров. Если вы хотите обнаружить переполнения со подписанными константами, используйте средство проверки Finder™ ошибок Polyspace Integer constant overflow.
Параметр:
-signed-integer-overflows |
Значение:
forbid | allow | warn-with-wrap-around |
По умолчанию:
forbid |
Пример (проверка кода):
polyspace-code-prover -sources |
Пример (сервер проверки кода):
polyspace-code-prover-server -sources |
-show-similar-overflows | Overflow | Overflow mode for unsigned integer (-unsigned-integer-overflows)