Выполните один или несколько из этих шагов до тех пор, пока не будет определено исправление для раздела с помощью нулевой проверки. Существует несколько способов исправить красный или оранжевый чек. Описание проверки и примеры кода см. в разделе Division by zero.
Иногда, особенно для оранжевой проверки, можно определить, что проверка представляет собой не реальную ошибку, а предположение Polyspace ®, которое не соответствует вашему коду. Если для смягчения предположения можно использовать опцию анализа, повторно запустите проверку с помощью этой опции. В противном случае в результат или код можно добавить комментарий и обоснование.
Общий рабочий процесс, применяемый ко всем проверкам, см. в разделе Интерпретация результатов проверки кода в пользовательском интерфейсе Polyspace Desktop.
Установите курсор на / или % операция, вызывающая нулевую ошибку деления.
Получите из подсказки следующую информацию:
Значения правого операнда (знаменателя).
В предыдущем примере правый операнд, val, имеет диапазон, содержащий ноль.
Возможное исправление: Чтобы избежать деления на ноль, выполните деление только в том случае, если val не равно нулю.
| Целое число | Плавающая точка |
|---|---|
if(val != 0)
func(1.0/val);
else
/* Error handling */ | #define eps 0.0000001
.
.
if(val < -eps || val > eps)
func(1.0/val);
else
/* Error handling */ |
Вероятная первопричина деления на ноль, если указано во всплывающей подсказке.
В предыдущем примере программное обеспечение идентифицирует упертую функцию, getVal, в качестве вероятной причины.
Возможное исправление: Чтобы избежать деления на ноль, ограничьте возвращаемое значение getVal. Например, укажите, что getVal возвращает значения в определенном диапазоне, например, 1..10. Чтобы задать ограничения, используйте опцию анализа Constraint setup (-data-range-specifications).
Перед / или % , проверьте, равен ли знаменатель нулю. Укажите соответствующую обработку ошибок, если знаменатель равен нулю.
Только если вы не ожидаете нулевого знаменателя, определите первопричину проверки. Трассировка потока данных, начиная с переменной знаменателя. Укажите точку, в которой можно задать ограничение для предотвращения нулевого значения.
В следующем примере трассировка потока данных, начиная с arg2:
void foo() {
double time = readTime();
double dist = readDist();
.
.
bar(dist,time);
}
void bar(double arg1, double arg2) {
double vel;
vel=arg1/arg2;
}bar вызывается с полным диапазоном значений.
Возможное исправление: Вызов bar только если его второй аргумент time больше нуля.
time получает полный диапазон значений из readTime.
Возможное исправление: Ограничение возвращаемого значения readTime, либо в теле readTime или через интерфейс спецификации ограничений Polyspace (Polyspace Constraint Specification), если у вас нет определения readTime. Дополнительные сведения см. в разделе Допущения о упорных функциях.
Чтобы отследить поток данных, выберите проверку и запишите информацию на панели Сведения о результате (Result Details).
Если на панели Сведения о результате (Result Details) отображается последовательность инструкций, которые приводят к проверке, выберите каждую инструкцию.
Если на панели Сведения о результате (Result Details) отображается номер строки вероятной причины проверки, щелкните правой кнопкой мыши панель Источник (Source). Выберите «Перейти к строке».
В противном случае:
Найдите предыдущую операцию записи для переменной операнда.
Пример: Значение arg2 записывается из значения time в bar.
При предыдущей операции записи определите новую переменную для обратной трассировки.
Установите курсор на переменные, участвующие в операции записи, чтобы увидеть их значения. Значения помогают выбрать переменную для трассировки.
Пример: В bar(dist,time), вы находите, что time имеет полный диапазон значений. Поэтому вы отслеживаете time.
Найдите предыдущую операцию записи для новой переменной. Таким образом можно продолжить трассировку до тех пор, пока не будет определена точка для задания ограничения.
Пример: Предыдущая операция записи на time является time=readTime(). Можно задать ограничение для возвращаемого значения readTime.
В зависимости от переменной используйте следующие сочетания клавиш навигации для поиска предыдущих экземпляров. В интерфейсе пользователя Polyspace можно выполнить только следующие действия.
| Переменная | Поиск предыдущих экземпляров переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов.
|
Глобальная переменная Щелкните правой кнопкой мыши переменную. Если отображается опция Показать в представлении доступа к переменной, переменная является глобальной переменной. |
|
Возвращаемое значение функции
ret=func(); |
|
Можно также определить, связаны ли переменные в какой-либо операции с какой-либо предыдущей операцией. См. раздел Поиск связей между переменными в коде.
Ищите общие причины Отдела нулевой проверкой.
Для переменной, которая должна быть ненулевой, проверьте, чтобы переменная в коде исключала нулевое значение.
В противном случае Polyspace не может определить, что переменная имеет ненулевые значения. Можно также задать ограничения вне кода. См. раздел Указание внешних ограничений.
При тестировании переменной для исключения ее нулевого значения проверьте, выполняется ли тест в уменьшенной области по сравнению с областью разделения.
Например, оператор assert(var !=0) происходит в if или while блок, но деление на var происходит вне блока. Если код не вводится if или while блок, assert не выполняется. Следовательно, за пределами if или while блок, Polyspace предполагает, что var все еще может быть равно нулю.
Возможное исправление:
Узнайте, почему тест выполняется в сокращенном объеме. В приведенном выше примере проверьте, можно ли разместить оператор assert(var !=0) за пределами if или for блок.
Если вы ожидаете if или while всегда выполнять, исследовать, когда он не выполняется.
Проверьте, можно ли отследить оранжевый чек по предположению Polyspace, которое встречается ранее в коде. Если предположение не соответствует действительности в вашем случае, добавьте комментарий или обоснование в результат или код. См. раздел Результаты анализа пространства адресов с помощью исправлений ошибок или обоснований.
Например, в коде используется изменчивая переменная. Затем:
Polyspace предполагает, что переменная является полной на каждом шаге кода. Диапазон включает ноль.
Деление на переменную может вызвать ошибку деления на ноль.
Если известно, что переменная принимает ненулевое значение, добавьте комментарий и обоснование, описывающие, почему вы не изменили код.
Дополнительные сведения см. в разделе Допущения анализа проверки кода.
Примечание
Прежде чем обосновывать проверку оранжевого цвета, тщательно продумайте, можно ли улучшить дизайн кода.
Эту проверку можно эффективно отключить. Если компилятор поддерживает бесконечности и NaNs из операций с плавающей запятой, можно включить режим проверки, который включает бесконечности и NaNs. Посмотрите Consider non finite floats (-allow-non-finite-floats).
