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