Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Division by zero. Существует несколько способов зафиксировать красную или оранжевую проверку. Для описания проверки и примеров кода, смотрите Division by zero.
Иногда, особенно для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать опцию анализа, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Программы автоматического доказательства Кода в Пользовательском интерфейсе Рабочего стола 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.
В противном случае:
Найдите предыдущую операцию записи на переменной операнда.
Пример: значение 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).
