Вы видите ошибки компиляции от заголовочных файлов, включенных Polyspace®.
Например, сообщение об ошибке относится к одной из подпапок
.polyspaceroot
\polyspace\verifier\cxx\include
Как правило, сообщение об ошибке связано со стандартной библиотечной функцией.
Если ваш компилятор задает стандартную библиотечную функцию или другое построение, и вы не обеспечиваете путь к своим заголовочным файлам компилятора, Polyspace использует свою собственную реализацию функции.
Если ваши определения компилятора отличаются от соответствующих определений Polyspace, остановок верификации с ошибкой.
Задайте папку, содержащую ваши заголовочные файлы компилятора.
В пользовательском интерфейсе добавьте папку в свой проект.
Для получения дополнительной информации смотрите, Добавляют Исходные файлы для Анализа в Пользовательском интерфейсе Polyspace (Polyspace Code Prover).
В командной строке используйте флаг -I
с polyspace-code-prover-server
команда.
Для получения дополнительной информации смотрите -I
.
Для компиляции с GNU® C на платформах UNIX®-based используйте /usr/include
. На встроенных компиляторах заголовочные файлы обычно находятся в подпапке папки установки компилятора. Примеры включают папки, даны для некоторых компиляторов.
Ветер River® Diab: Например, /apps/WindRiver/Diab/5.9.4/diab/5.9.4.8/include/
.
IAR Встроенные Инструментальные средства: Например, C:\Program Files\IAR Systems\Embedded Workbench 7.5\arm\inc
.
Microsoft® Visual Studio®: Например, C:\Program Files\Microsoft Visual Studio 14.0\VC\include
.
Консультируйтесь со своей документацией компилятора для пути к вашим заголовочным файлам компилятора. В качестве альтернативы смотрите, Обеспечивают Стандартные Заголовки Библиотеки для Анализа Polyspace.