Анализ Средства поиска Ошибки по умолчанию не возвращает дефект, вызванный специальным значением неизвестного входа, если вход не ограничен. Polyspace не делает предположения о значении неограниченных входных параметров, когда ваш исходный код является неполным. Например, в следующем Средстве поиска Ошибки кода обнаруживает division by zero в foo_1(), но не в foo_2():
int foo_1(int p)
{
int x = 0;
if ( p > -10 && p < 10 ) /* p is bounded by if statement */
x = 100/p; /* Division by zero detected */
return x;
}
int foo_2(int p) /* p is unbounded */
{
int x = 0;
x = 100/p; /* Division by zero not detected */
return x;
} Чтобы установить границы на вашем входе, добавьте ограничения в своем коде, такие как assert или if. За счет возможно более длинного времени выполнения можно выполнить более исчерпывающий анализ, где все значения входных параметров функции рассматриваются при показе дефектов. Смотрите Расширяют Средства проверки Средства поиска Ошибки, чтобы Найти Дефекты от Определенных Системных Входных значений.
Аналитические предположения средства поиска ошибки | Глобальные переменные в Polyspace Bug Finder