Анализ Средства поиска Ошибки не возвращает дефект, вызванный специальным значением неизвестного входа, если вход не ограничен. 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