В результатах проверки стандартная математическая функция библиотеки ведет себя не так, как ожидалось.
Например, оператор assert(isinf(x)) не ограничивает значение x к положительной или отрицательной бесконечности в последующих высказываниях.
Если Polyspace ® не может найти определения математических функций, проверка использует реализации Polyspace стандартных математических функций библиотеки.
В некоторых случаях реализация функции Polyspace может не соответствовать спецификации функции. Следует отметить, что в таких случаях реализация Polyspace чрезмерно приближает поведение функции. Например, после оператора assert(isinf(x)), диапазон значений x включают положительную и отрицательную бесконечность. Поэтому такое поведение не приводит к зеленым проверкам операций, которые могут вызвать ошибки во время выполнения.
Явно укажите путь к собственным файлам заголовка компилятора, чтобы при проверке использовались реализации функций компилятора. Например, некоторые компиляторы реализуют такие функции, как isinf в виде макросов в своих файлах заголовков.
Если выполняется проверка из командной строки, используйте параметр -I.
Если выполняется проверка из интерфейса пользователя, см. раздел Добавление исходных файлов для анализа в интерфейсе пользователя Polyspace.
При использовании перекрестного компилятора и создании проекта Polyspace из системы сборки в проекте используются файлы заголовков, предоставленные компилятором.