Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Division by zero. Существует несколько способов исправить красный или оранжевый чек. Для получения описания примеров проверки и кода смотрите Division by zero.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
Поместите курсор на / или % операция, которая вызывает ошибку Division by zero.
Получите следующую информацию из подсказки:
Значения правого операнда (знаменателя).
В предыдущем примере правый операнд, 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 Constraint Specification, если у вас нет определения readTime. Для получения дополнительной информации смотрите Допущения об упрямых функциях.
Чтобы проследить поток данных, выберите проверку и отметьте информацию на панели Result Details.
Если на панели Result Details отображается последовательность команд, ведущих к проверке, выберите каждую инструкцию.
Если на панели Result Details отображается номер линии вероятной причины проверки, щелкните правой кнопкой мыши на панели Source. Выберите Go To Line.
В противном случае:
Найдите предыдущую операцию записи переменной operand.
Пример: Значение arg2 записывается из значения time в bar.
При предыдущей операции записи идентифицируйте новую переменную для трассировки назад.
Поместите курсор на переменные, участвующие в операции записи, чтобы увидеть их значения. Значения помогают вам решить, какую переменную трассировать.
Пример: В bar(dist,time), вы находите, что time имеет полный диапазон значений. Поэтому вы отслеживаете time.
Найдите предыдущую операцию записи новой переменной. Продолжите трассировку таким образом, пока вы не идентифицируете точку, чтобы задать свое ограничение.
Пример: Предыдущая операция записи на time является time=readTime(). Можно принять решение задать ограничение на возврат значение readTime.
В зависимости от переменной используйте следующие навигационные ярлыки для поиска предыдущих образцов. Можно выполнить следующие шаги только в пользовательском интерфейсе Polyspace.
| Переменная | Как найти предыдущие образцы переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов:
|
Глобальная переменная Щелкните правой кнопкой мыши переменную. Если появляется Show In Variable Access View опция, переменная является глобальной переменной. |
|
Функция возврата значение
ret=func(); |
|
Можно также определить, связаны ли переменные в любой операции с какой-либо предыдущей операцией. См. Раздел «Поиск отношений между переменными в коде».
Проверьте общие причины проверки Division by zero.
Для переменной, которая, как вы ожидаете, будет ненулевой, смотрите, проверяете ли вы переменную в вашем коде, чтобы исключить нулевое значение.
В противном случае Polyspace не может определить, что переменная имеет ненулевые значения. Можно также задать ограничения вне вашего кода. См. «Задание внешних ограничений».
Если вы проверяете переменную, чтобы исключить ее нулевое значение, смотрите, происходит ли тест в уменьшенных возможностях по сравнению с возможностями деления.
Для примера, оператор assert(var !=0) происходит в if или while блок, но деление на var находится вне блока. Если код не вводит if или while блок, assert не выполняется. Поэтому за пределами if или while блок, Polyspace принимает, что var все еще может быть нулем.
Возможное исправление:
Исследуйте, почему тест происходит в ограниченных возможностях. В приведенном выше примере проверьте, можно ли разместить оператор assert(var !=0) вне if или for блок.
Если вы ожидаете if или while блок, который нужно всегда выполнять, исследуйте, когда он не выполняется.
Посмотрите, можно ли проследить оранжевую проверку до допущения Polyspace, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
Например, вы используете изменчивую переменную в своем коде. Затем:
Polyspace принимает, что переменная является полной области значений на каждом шаге в коде. В область значений входят нули.
Деление на переменную может вызвать Division by zero ошибку.
Если вы знаете, что переменная принимает ненулевое значение, добавьте комментарий и обоснование, описывающие, почему вы не изменили код.
Для получения дополнительной информации смотрите Допущения анализа Code Prover.
Примечание
Прежде чем обосновывать оранжевую проверку, внимательно рассмотрим, сможете ли вы улучшить свои проекты кодирования.
Можно эффективно отключить эту проверку. Если ваш компилятор поддерживает бесконечности и NaNs от операций с плавающей точкой, можно включить режим верификации, который включает бесконечности и NaNs. См. Consider non finite floats (-allow-non-finite-floats).
