Перед верификацией укажите язык исходного кода (C или C++), целевой процессор и компилятор, который вы используете для создания своего кода. В некоторых случаях, чтобы эмулировать поведение компилятора, вам, возможно, придется задать дополнительные опции.
Используя вашу спецификацию, верификация определяет размеры фундаментальных типов, рассматривает определенные макросы как определенные и интерпретирует специфические для компилятора расширения Стандарта. Если опции не соответствуют вашему окружению во время выполнения, можно встретить:
Ошибки компиляции
Результаты верификации, которые могут не применяться к вашему целевому объекту
Если вы используете команду сборки, такую как gmake чтобы создать код, и команда build соответствует определенным ограничениям, можно извлечь опции из команды build. В противном случае опции задаются явным образом.
Если вы используете скрипты автоматизации сборки для создания исходного кода, можно настроить Polyspace® проект из ваших скриптов. Опции, связанные с вашим компилятором, заданы в этом проекте.
В десктопных продуктах Polyspace для получения информации о том, как отследить команду build из:
Пользовательский интерфейс Polyspace, см., Добавление исходных файлов для анализа в пользовательском интерфейсе Polyspace.
DOS или UNIX® командная строка, см. polyspace-configure.
MATLAB® командная строка, см. polyspaceConfigure.
В серверных продуктах Polyspace для получения информации о том, как отследить команду build, смотрите Создание строения анализа Polyspace из Build Command (Polyspace Code Prover Server).
Для создания проекта Polyspace, ваш скрипт автоматизации сборки (make-файл) должен соответствовать определенным требованиям. Смотрите требования к созданию проектов из систем сборки.
Если вы не можете проследить команду build и поэтому вручную создать проект, необходимо задать опции явным образом.
В пользовательском интерфейсе десктопных продуктов Polyspace выберите строение проекта. На панели Configuration выберите Target & Compiler. Задайте опции.
В командной строке DOS или UNIX задайте флаги с polyspace-bug-finder, polyspace-code-prover, polyspace-bug-finder-server (Polyspace Bug Finder Server) или polyspace-code-prover-server (Polyspace Code Prover Server) команда.
В командной строке MATLAB задайте аргументы с polyspaceBugFinder, polyspaceCodeProver, polyspaceBugFinderServer или polyspaceCodeProverServer функция.
Задайте опции в этом порядке.
Необходимые опции:
Source code language (-lang): Если все файлы имеют одинаковое расширение .c или .cpp, верификация использует расширение для определения языка исходного кода. В противном случае явным образом задайте опцию.
Compiler (-compiler): Выберите компилятор, который вы используете для создания исходного кода. Если вы не можете найти компилятор, используйте опцию, которая тесно соответствует вашему компилятору.
Target processor type (-target): Укажите целевой процессор, на котором вы собираетесь выполнять свой код. Для некоторых процессоров можно изменить спецификации по умолчанию. Для образца, для процессора hc08можно изменить размер типов double и long double от 32 до 64 бит.
Если вы не можете найти свой целевой процессор, можно создать свой собственный целевой объект и указать размеры фундаментальных типов, сигнальность по умолчанию char, и конечность целевой машины. См. Generic target options.
Языковые опции:
C standard version (-c-version): Стандарт языка C по умолчанию зависит от спецификации компилятора. Если вы явным образом не задаете компилятор, в анализе по умолчанию используется стандарт 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 компилятор, вы должны задать путь к файлам заголовка компилятора. Смотрите раздел «Предоставление заголовков стандартных библиотек для анализа Polyspace».
Если после выполнения анализа вы все еще видите ошибки компиляции, вам, возможно, придется задать другие опции:
Задайте макросы: Иногда возникает ошибка компиляции, поскольку анализ рассматривает макрос как неопределенный. Явно задайте эти макросы. См. Preprocessor definitions (-D).
Укажите файлы включения: Иногда ошибка компиляции возникает, потому что ваш компилятор определяет стандартные функции библиотеки по-другому по сравнению с Polyspace, и вы не предоставляете файлы включения компилятора. Явным образом укажите путь к файлам включения компилятора. Смотрите раздел «Предоставление заголовков стандартных библиотек для анализа Polyspace».
C standard version (-c-version) | C++ standard version (-cpp-version) | Compiler (-compiler) | Preprocessor definitions (-D) | Source code language (-lang) | Target processor type (-target)
