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