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