Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Overflow. Существует несколько способов исправить проверку. Для получения описания примеров проверки и кода смотрите Overflow.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
Поместите курсор на операцию, которая переполнена.
Получите следующую информацию из подсказки:
Переменная operand, которую можно ограничить, чтобы избежать переполнения.
В предыдущем примере левый операнд, val, имеет полную область значений значений.
Возможное исправление: Чтобы избежать переполнения, выполните умножение только если val находится в определенной области значений.
if(val < INT_MAX/2)
return(val*2);
else
/* Alternate action */Вероятная первопричина переполнения, если указано в подсказке.
В предыдущем примере программное обеспечение идентифицирует упорную функцию getVal, как вероятную причину.
Возможное исправление: Чтобы избежать переполнения, ограничьте возврат значение getVal. Для образца задайте, что getVal возвращает значения в определенной области значений, например 1..10. Для получения дополнительной информации смотрите Допущения об упрямых функциях.
Проследите поток данных, начиная с переменной operand, которую вы хотите ограничить. Определите подходящую точку, чтобы задать ваше ограничение.
В следующем примере проследите поток данных, начиная с tempVal.
val = func();
.
.
tempVal = val;
.
.
tempVal++ ;tempVal получает полный диапазон значений от val.
Возможное исправление: Назначить val на tempVal только если val меньше определенного значения.
val получает полный диапазон значений от func.
Возможное исправление: Ограничение возвращаемого значения func, либо в теле func или через интерфейс Polyspace Constraint Specification, если func упрямый. Для получения дополнительной информации смотрите Допущения об упрямых функциях.
Чтобы проследить поток данных, выберите проверку и отметьте информацию на панели Result Details.
Если на панели Result Details отображается последовательность команд, ведущих к проверке, выберите каждую инструкцию.
Если на панели Result Details отображается номер линии вероятной причины проверки, щелкните правой кнопкой мыши на панели Source. Выберите Go To Line.
В противном случае:
Найдите предыдущую операцию записи переменной operand.
Пример: Предыдущая операция записи на tempVal является tempVal=val.
При предыдущей операции записи идентифицируйте новую переменную для трассировки назад.
Поместите курсор на переменные, участвующие в операции записи, чтобы увидеть их значения. Значения помогают вам решить, какую переменную трассировать.
Пример: В tempVal=val, вы находите, что val имеет полный диапазон значений. Поэтому вы отслеживаете val.
Найдите предыдущую операцию записи новой переменной. Продолжите трассировку таким образом, пока вы не идентифицируете точку, чтобы задать свое ограничение.
Пример: Предыдущая операция записи на val является val=func(). Можно принять решение задать ограничение на возврат значение func.
В зависимости от переменной используйте следующие навигационные ярлыки для поиска предыдущих образцов. Можно выполнить следующие шаги только в пользовательском интерфейсе Polyspace.
| Переменная | Как найти предыдущие образцы переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов:
|
Глобальная переменная Щелкните правой кнопкой мыши переменную. Если появляется Show In Variable Access View опция, переменная является глобальной переменной. |
|
Функция возврата значение
ret=func(); |
|
Можно также определить, связаны ли переменные в любой операции с какой-либо предыдущей операцией. См. Раздел «Поиск отношений между переменными в коде».
Совет
Чтобы различить целое число и переполнение с плавающей точкой, используйте столбец Detail на панели Results List. Щелкните заголовок столбца, чтобы целое число и переполнение с плавающей точкой были сгруппированы. Если Вы не видите Detail столбец, щелкните правой кнопкой мыши по любому другому заголовку столбца и позвольте этот столбец.
Если операция, вызывающая переполнение, происходит в цикле или в теле рекурсивной функции:
Проверьте, можно ли уменьшить количество запусков или рекурсий.
Посмотрите, можно ли поместить условие выхода в цикл или рекурсивную функцию перед переполнением операции.
Посмотрите, можно ли проследить оранжевую проверку до допущения Polyspace, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
Например, вы используете изменчивую переменную в своем коде. Затем:
Polyspace принимает, что изменчивая переменная является полной области значений на каждом шаге в коде.
Операция, использующая эту переменную, может переполниться и поэтому является оранжевой.
Если вы знаете, что переменная принимает меньшую область значений значений, добавьте в код комментарий и обоснование с описанием того, почему вы не изменили код.
Для получения дополнительной информации смотрите Допущения анализа Code Prover.
Примечание
Прежде чем обосновывать оранжевую проверку, внимательно рассмотрим, сможете ли вы улучшить свои проекты кодирования.
