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