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