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