Вы видите ошибки компиляции из файлов заголовков, включенных в 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 ® Visual Studio ®: Например,C:\Program Files\Microsoft Visual Studio 14.0\VC\include.
Путь к файлам заголовков компилятора см. в документации компилятора. Также см. раздел Предоставление стандартных заголовков библиотек для анализа в пространстве.