Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки 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)
.