Перед проверкой укажите язык исходного кода (C или C++), целевой процессор и компилятор, используемый для создания кода. В некоторых случаях для эмуляции поведения компилятора может потребоваться указать дополнительные параметры.
С помощью спецификации проверка определяет размеры фундаментальных типов, рассматривает определенные макросы как определенные и интерпретирует специфичные для компилятора расширения стандарта. Если параметры не соответствуют среде выполнения, можно столкнуться с:
Ошибки компиляции
Результаты проверки, которые могут не применяться к конечному объекту
Если используется команда построения, например gmake для создания кода, а команда build отвечает определенным ограничениям, можно извлечь параметры из команды build. В противном случае явно задайте параметры.
Если для создания исходного кода используются сценарии автоматизации построения, можно настроить проект Polyspace ® на основе сценариев. Параметры, связанные с компилятором, указаны в этом проекте.
В продуктах для настольных ПК Polyspace для получения информации об отслеживании команды build см.:
Интерфейс пользователя Polyspace см. в разделе Добавление исходных файлов для анализа в интерфейсе пользователя Polyspace.
DOS или UNIX ®, см.polyspace-configure.
Командная строка MATLAB ®, см.polyspaceConfigure.
Сведения о трассировке команды build см. в разделе Создание конфигурации анализа Polyspace из команды Build (Polyspace Code Prover Server).
Для создания проекта Polyspace сценарий автоматизации сборки (makefile) должен соответствовать определенным требованиям. См. раздел Требования к созданию проекта из Build Systems.
Если невозможно отследить команду build и, следовательно, вручную создать проект, необходимо явно указать параметры.
В интерфейсе пользователя настольных продуктов Polyspace выберите конфигурацию проекта. На панели Конфигурация выберите Целевой & компилятор. Задайте параметры.
В командной строке DOS или UNIX укажите флаги с помощью polyspace-bug-finder, polyspace-code-prover, polyspace-bug-finder-server(сервер поиска ошибок Polyspace) или polyspace-code-prover-server(Сервер проверки кода Polyspace).
В командной строке MATLAB укажите аргументы с помощью polyspaceBugFinder, polyspaceCodeProver, polyspaceBugFinderServer или polyspaceCodeProverServer функция.
Укажите параметры в этом порядке.
Обязательные параметры:
Source code language (-lang): Если все файлы имеют одинаковое расширение .c или .cpp, проверка использует расширение для определения языка исходного кода. В противном случае явно укажите параметр.
Compiler (-compiler): Выберите компилятор, используемый для создания исходного кода. Если компилятор не найден, используйте параметр, точно соответствующий компилятору.
Target processor type (-target)Укажите целевой процессор, на котором предполагается выполнить код. Для некоторых процессоров можно изменить спецификации по умолчанию. Например, для процессора hc08, можно изменить размер типов double и long double от 32 до 64 бит.
Если вы не можете найти целевой процессор, вы можете создать свой собственный целевой и указать размеры фундаментальных типов, по умолчанию signedness charи endianness целевой машины. Посмотрите Generic target options.
Языковые параметры:
C standard version (-c-version): Стандарт языка Си по умолчанию зависит от спецификации компилятора. Если явно не указать компилятор, в анализе по умолчанию используется стандарт C99. Укажите более ранний стандарт, например C90, или более поздний стандарт, например C11.
C++ standard version (-cpp-version): Стандарт языка C++ по умолчанию зависит от спецификации компилятора. Если явно не указать компилятор, в анализе по умолчанию используется стандарт C++ 03. Укажите более поздние стандарты, такие как C++ 11 или C++ 14.
Параметры компилятора:
Доступность этих опций зависит от спецификации для Compiler (-compiler). Например, при выборе visual компилятор, параметр Pack alignment value (-pack-alignment-value) доступен. С помощью этого параметра можно эмулировать параметр компилятора. /Zp которая используется в Visual Studio ®.
Все параметры компилятора см. в разделе Цель и компилятор.
Дополнительные параметры:
С помощью этих опций можно изменить результаты проверки. Например, при использовании опции Division round down (-div-round-down), проверка считает, что частные от деления или модуля отрицательных чисел округляются вниз. Эти параметры используются только в том случае, если при компиляции кода используются аналогичные параметры.
Все дополнительные параметры см. в разделе Цель и компилятор.
Заголовочные файлы компилятора:
При указании diab, tasking или greenhills необходимо указать путь к файлам заголовка компилятора. См. раздел Предоставление стандартных заголовков библиотек для анализа полиспейсов.
Если после выполнения анализа все еще появляются ошибки компиляции, может потребоваться указать другие параметры:
Определение макросов: Иногда возникает ошибка компиляции, поскольку анализ считает макрос неопределенным. Явно определите эти макросы. Посмотрите Preprocessor definitions (-D).
Укажите include files: Иногда возникает ошибка компиляции, поскольку компилятор определяет стандартные библиотечные функции иначе, чем Polyspace, и вы не предоставляете компилятору include files. Явно укажите путь к включаемым файлам компилятора. См. раздел Предоставление стандартных заголовков библиотек для анализа полиспейсов.
C standard version (-c-version) | C++ standard version (-cpp-version) | Compiler (-compiler) | Preprocessor definitions (-D) | Source code language (-lang) | Target processor type (-target)