Когда вы запускаете Polyspace® как часть ваших процессов разработки программного обеспечения, ваши аналитические скрипты должны быть предварительно сконфигурированы для новых представлений кода. Например, новые исходные файлы должны быть автоматически включены в анализ Polyspace. Чтобы держать аналитическую настройку в курсе с новыми представлениями, можно усилить существующие артефакты, такие как команда сборки (make-файлы) и создать аналитическую настройку на лету, когда новые представления происходят.
Аналитическая настройка состоит из двух частей:
Опции связаны с исходным кодом и целью, такие как размеры типа данных, макроопределения, циклические задачи и прерывания, и так далее.
Опции связаны с анализом, такие как средства проверки, предположения верификации кода, и так далее.
Наиболее распространенные опции, связанные с исходным кодом и целью:
-sources-list-file: Задайте текстовый файл, содержащий один исходный файл на строку.
-I: Задайте папки, содержащие включенные заголовочные файлы.
Compiler (-compiler): Задайте компилятор, используемый в создании вашего исходного кода.
Target processor type (-target): Задайте размеры типов данных и порядка байтов путем выбора предопределенного целевого процессора.
Preprocessor definitions (-D): Замените нераспознанный код в целях анализа Polyspace. Вы обычно используете эту опцию, если анализ показывает ошибки компиляции от специфичных для компилятора ключевых слов и макросов.
Constraint setup (-data-range-specifications): Задайте внешние ограничения на глобальные переменные и функциональные интерфейсы. Опция обычно полезна для более точного анализа Программы автоматического доказательства Кода.
Для полного списка опций см.:
Аналитические опции (Polyspace Code Prover Server)
В непрерывном рабочем процессе интегрирования вы обычно не задаете аргументы опции явным образом. Ваша команда сборки содержит технические требования для источников, компилятор, макроопределения и так далее. Запустите polyspace-configure команда, чтобы извлечь эти технические требования из вашей команды сборки и создать файл опций. Например, если вы используете make чтобы создать ваш исходный код, запустите анализ можно следующим образом:
polyspace-configure -output-options-file polyspace_opts make polyspace-bug-finder-server -options-file polyspace_opts polyspace-code-prover-server -options-file polyspace_opts |
Первая команда извлекает входные и выходные технические требования путем выполнения инструкций в make-файле и создает аналитический файл опций. Вторые и третьи команды запускают анализ Программы автоматического доказательства Средства поиска и Кода Ошибки с файлом опций. Смотрите Создают Аналитическую Настройку Polyspace из Команды Сборки.
Если вы не можете извлечь опции из своей команды сборки, задайте опции явным образом. Можно создать некоторые аргументы опции на лету от новых представлений. Например, аргумент для опции -sources-list-file текстовый файл, который перечисляет источники. Можно обновить этот текстовый файл на основе любого нового исходного файла, добавленного к репозиторию исходного кода.
Если необходимо задать целевые и параметры компилятора явным образом, вы не можете разобраться во всех опциях на первом показе. Найти правильную комбинацию опций:
Задайте опции Compiler (-compiler) и Target processor type (-target) в вашем файле опций.
Скомпилируйте код со своим компилятором и зафиксируйте все ошибки компиляции. Затем запуск только часть компиляции анализа Polyspace.
В Средстве поиска Ошибки отключите все средства проверки. Задайте -checkers none в файле опций. Смотрите Find defects (-checkers).
В Программе автоматического доказательства Кода остановите анализ после компиляции. Задайте -to compile в файле опций. Смотрите Verification level (-to).
Если вы сталкиваетесь с ошибками компиляции, вам придется работать вокруг ошибок с опциями Polyspace. Например, если вы видите ошибку компиляции потому что макро-_WIN32 задан с параметром компилятора, но Polyspace рассматривает макрос как неопределенный по умолчанию, эмулируйте свой параметр компилятора с опцией Polyspace -D _WIN32. Смотрите Цель и Компилятор, Макросы и Параметры среды для целевых и параметров компилятора.
Если вы фиксируете все ошибки компиляции с аналитическими опциями Polyspace, ваш файл опций подготовлен с правильным набором опций Polyspace для анализа.
Если у вас есть установка десктопных решений, Polyspace Bug Finder™ и/или Polyspace Code Prover™, можно выполнить пробные прогоны в пользовательском интерфейсе десктопных решений. Можно затем сгенерировать файл опций от настройки, заданной в пользовательском интерфейсе. Пользовательский интерфейс обеспечивает различные функции, такие как:
Ассистент компиляции, который предлагает обходные решения для некоторых ошибок компиляции,
Автоматическая генерация XML-файла для ограничительной спецификации,
Контекстно-зависимая справка для опций,
Смотрите конфигурируют аналитические опции Polyspace в пользовательском интерфейсе и генерируют скрипты.
Некоторые опции, связанные с анализом Polyspace:
Средство поиска ошибки
Find defects (-checkers): Задайте средства проверки, чтобы включить для анализа Средства поиска Ошибки.
Check MISRA C:2012 (-misra3) и другие опции, связанные с внешними стандартами: Задайте внешний стандарт и предопределенное подмножество того стандарта.
Set checkers by file (-checkers-selection-file): Задайте пользовательское подмножество правил из внешних стандартов.
Bug Finder and Code Prover report (-report-template): Укажите, что PDF, Word или отчет HTML должны быть сгенерированы наряду с результатами анализа и задать шаблон для отчета.
Программа автоматического доказательства кода
Overflow mode for signed integer (-signed-integer-overflows): Задайте поведение после переполнения: остановите анализ или продолжите перенос.
Detect stack pointer dereference outside scope (-detect-pointer-escape): Задайте, должен ли анализ найти случаи, куда функция возвращает указатель на одну из его локальных переменных.
Detect uncalled functions (-uncalled-function-checks): Задайте, должен ли анализ отметить функции, которые не вызваны прямо или косвенно от основного или другой функции точки входа.
Bug Finder and Code Prover report (-report-template): Укажите, что PDF, Word или отчет HTML должны быть сгенерированы наряду с результатами анализа и задать шаблон для отчета.
Средства проверки и другие опции, связанные с анализом Polyspace, могут быть применимы больше чем к одному проекту. Чтобы выпустить универсальные стандарты через проекты, можно снова использовать это подмножество аналитических опций. При выполнении анализа задайте два файла опций, один содержащий опции, характерные для текущего проекта и другого содержащего допускающие повторное использование опции. Можно извлечь файл прав преимущественной покупки из команды сборки, но явным образом создать второй файл опций.
Например, в этом примере, polyspace-bug-finder-server команда использует два файла опций: compile_opts сгенерированный от make-файла и runbf_opts созданный вручную. Все допускающие повторное использование опции могут быть заданы в runbf_opts.
polyspace-configure -output-options-file compile_opts make polyspace-bug-finder-server -options-file compile_opts -options-file runbf_opts polyspace-code-prover-server -options-file compile_opts -options-file runcp_opts |
Если та же опция появляется в двух файлах опций, последний экземпляр опции рассматривается. В предыдущем примере, если опция происходит в обоих compile_opts и runbf_opts, вхождение в runbf_opts рассматривается. Если вы хотите заменить предыдущие случаи опции, используйте файл дополнительных опций со своими переопределениями. Добавьте этот файл опций в конец аналитической команды.
polyspace-bug-finder-server | polyspace-configure
