Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Division by zero. Существует несколько способов зафиксировать красную или оранжевую проверку. Для описания проверки и примеров кода, смотрите Division by zero.
Иногда, специально для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать аналитическую опцию, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Polyspace Code Prover.
Установите свой курсор на операцию / или %, которая вызывает ошибку 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.
В противном случае:
Найдите предыдущую операцию записи на переменной операнда.
Пример: значение 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, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Комментарии.
Например, вы используете энергозависимую переменную в своем коде. Затем:
Polyspace принимает, что переменная является полным диапазоном на каждом шаге в коде. Область значений включает нуль.
Деление переменной может вызвать ошибку Division by zero.
Если вы знаете, что переменная берет ненулевое значение, добавьте комментарий и выравнивание, описывающее, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Аналитические Предположения Программы автоматического доказательства Кода.
Прежде, чем выровнять по ширине оранжевую проверку, рассмотрите тщательно, можно ли улучшить проект кодирования.
Можно эффективно отключить эту проверку. Если ваш компилятор поддерживает бесконечности и NaNs от операций с плавающей точкой, можно включить режим верификации, который включает бесконечности и NaNs. Смотрите Consider non finite floats (-allow-non-finite-floats).
