Перед Polyspace® анализирует код на ошибки и ошибки времени выполнения, он компилирует ваш код. Даже если код компилируется с вашим компилятором, можно увидеть ошибки компиляции с Polyspace. Если ошибка происходит от стандартной функции библиотеки, это обычно указывает, что Polyspace не использует ваши заголовки компилятора. Чтобы обойти ошибки, укажите путь к заголовкам компилятора.
В этом разделе показано, как найти стандартные заголовки библиотеки от вашего компилятора. Примеры кода вызывают ошибку компиляции, которая показывает расположение заголовков.
Чтобы найти папку, содержащую системные заголовки компилятора C, скомпилируйте этот код С с помощью набора инструментов компиляции:
float fopen(float f); #include <stdio.h>
Код не компилируется, потому что fopen объявление конфликтует с объявлением внутри stdio.h. Ошибка компиляции показывает расположение вашей реализации компилятора stdio.h. Все заголовки стандартных библиотек на C могут находиться в этой папке.
Чтобы найти папку, содержащую системные заголовки C++ компилятора, скомпилируйте этот код С++ с помощью набора инструментов компиляции:
namespace std {
float cin;
}
#include <iostream>
cin объявление конфликтует с объявлением внутри iostream.h. Ошибка компиляции показывает расположение вашей реализации компилятора iostream.h. Все заголовки стандартной библиотеки C++ могут находиться в этой папке.
После нахождения пути к файлам заголовков компилятора укажите путь для анализа Polyspace. Для кода С++ укажите пути к заголовкам C и C++.
В пользовательском интерфейсе (Polyspace рабочего стола продукты) добавьте папку к своему проекту.
Для получения дополнительной информации см. раздел «Добавление исходных файлов для анализа» в интерфейсе пользователя Polyspace.
В командной строке используйте флаг -I с polyspace-bug-finder, polyspace-code-prover (Polyspace Code Prover), polyspace-bug-finder-server (Polyspace Bug Finder Server) или polyspace-code-prover-server (Polyspace Code Prover Server) команда..
Для получения дополнительной информации смотрите -I.