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