Покажите все переполнение во всеобъемлющем режиме
-show-similar-overflows
-show-similar-overflows причины все переполнение, которое покажут во всеобъемлющем режиме, даже если они происходят из той же первопричины.
Если вы выбираете warn-with-wrap-around для опции Overflow mode for signed integer (-signed-integer-overflows) или Overflow mode for unsigned integer (-unsigned-integer-overflows), значения, что переполнение перенесено. Например, значение INT_MAX + 1 повторяется к INT_MIN. Путь с переполняющимся значением продолжается вне переполнения перенесенным значением и может привести к подобному переполнению несколько линий позже. По умолчанию Программа автоматического доказательства Кода обнаруживает переполнение от той же первопричины и показывает только первое из подобного переполнения. Если вы фиксируете это переполнение, последующее переполнение также фиксируется. Если вы хотите видеть все переполнение во всеобъемлющем режиме, используйте опцию -show-similar-overflows.
Если при запуске анализ от пользовательского интерфейса (только десктопные решения Polyspace®) на панели Configuration, можно ввести эту опцию в поле Other. Смотрите Other.
В этом примере, значении var неизвестно, и случаи ребра могут привести к переполнению в операции *copy1 = var * 2. Те же случаи ребра также приводят к переполнению в следующей операции. Программа автоматического доказательства кода показывает, что оранжевый Overflow проверяет первую операцию только.
int input();
void getEven(int* copy1, int* copy2) {
int var;
var = input();
*copy1 = var * 2;
*copy2 = var * 2;
}Если вы используете опцию -show-similar-overflows, Программа автоматического доказательства кода показывает, что оранжевый Overflow проверяет обе операции.
int input();
void getEven(int* copy1, int* copy2) {
int var;
var = input();
*copy1 = var * 2;
*copy2 = var * 2;
}-options-file | Overflow mode for signed integer (-signed-integer-overflows) | Overflow mode for unsigned integer (-unsigned-integer-overflows) | Overflow (Polyspace Code Prover Access)