Перед верификацией задайте свой язык исходного кода (C или C++), целевой процессор и компилятор, который вы используете в создании вашего кода. В определенных случаях, чтобы эмулировать ваше поведение компилятора, вам придется задать дополнительные опции.
Используя вашу спецификацию, верификация определяет размеры фундаментальных типов, рассматривает определенные макросы, как задано и интерпретирует специфичные для компилятора расширения Стандарта. Если опции не соответствуют вашей среде выполнения, можно столкнуться:
Ошибки компиляции
Результаты верификации, которые не могут примениться к вашей цели
Если вы используете команду сборки, такую как gmake создавать ваш код и команду сборки соответствует определенным ограничениям, можно извлечь опции из команды сборки. В противном случае задайте опции явным образом.
Если вы используете скрипты автоматизации сборки, чтобы создать ваш исходный код, можно настроить проект Polyspace® из скриптов. Опции, сопоставленные с вашим компилятором, заданы в том проекте.
В десктопных решениях Polyspace, для получения информации о том, как проследить вашу команду сборки от:
Пользовательский интерфейс Polyspace, смотрите, Добавляют Исходные файлы для Анализа в Пользовательском интерфейсе Polyspace.
DOS или командная строка UNIX®, смотрите polyspace-configure.
Командная строка MATLAB®, смотрите polyspaceConfigure.
В серверных продуктах Polyspace, для получения информации о том, как проследить вашу команду сборки, видят, Создают Аналитическую Настройку Polyspace из Команды Сборки (Polyspace Code Prover Server).
Для создания проекта Polyspace ваш скрипт автоматизации сборки (make-файл) должен удовлетворить определенные требования. Смотрите Требования для Создания Проекта от Систем сборки.
Если вы не можете проследить свою команду сборки и поэтому вручную создать проект, необходимо задать опции явным образом.
В пользовательском интерфейсе десктопных решений Polyspace выберите настройку проекта. На панели Configuration выберите Target & Compiler. Задайте опции.
В DOS или командной строке UNIX, задайте флаги с polyspace-bug-finder, polyspace-code-prover, polyspace-bug-finder-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 то, что вы используете в Визуальном 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)
