Анализ Bug Finder по умолчанию не возвращает дефект, вызванный специальным значением неизвестного входа, если вход не ограничен. Polyspace не делает предположения о значении неограниченных входных данных, когда исходный код неполный. Например, в следующем коде Bug Finder обнаруживает деление на ноль в 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