Подготовьте скрипты к анализу Polyspace

Когда вы запускаете Polyspace® как часть ваших процессов разработки программного обеспечения, ваши аналитические скрипты должны быть предварительно сконфигурированы для новых представлений кода. Например, новые исходные файлы должны быть автоматически включены в анализ Polyspace. Чтобы держать аналитическую настройку в курсе с новыми представлениями, можно усилить существующие артефакты, такие как команда сборки (make-файлы) и создать аналитическую настройку на лету, когда новые представления происходят.

Аналитическая настройка состоит из двух частей:

  • Опции связаны с исходным кодом и целью, такие как размеры типа данных, макроопределения, циклические задачи и прерывания, и так далее.

  • Опции связаны с анализом, такие как средства проверки, предположения верификации кода, и так далее.

Опции, связанные с исходным кодом и целью

Наиболее распространенные опции, связанные с исходным кодом и целью:

  • -sources-list-file: Задайте текстовый файл, содержащий один исходный файл на строку.

  • -I: Задайте папки, содержащие включенные заголовочные файлы.

  • Compiler (-compiler): Задайте компилятор, используемый для создания вашего исходного кода.

  • Target processor type (-target): Задайте размеры типов данных и порядка байтов путем выбора предопределенного целевого процессора.

  • Preprocessor definitions (-D): Замените нераспознанный код в целях анализа Polyspace. Вы обычно используете эту опцию, если анализ показывает ошибки компиляции от специфичных для компилятора ключевых слов и макросов.

  • Constraint setup (-data-range-specifications): Задайте внешние ограничения на глобальные переменные и функциональные интерфейсы. Опция обычно полезна для более точного анализа Программы автоматического доказательства Кода.

Для полного списка опций см.:

Извлеките опции из команды сборки

В непрерывном рабочем процессе интегрирования вы обычно не задаете аргументы опции явным образом. Ваша команда сборки содержит технические требования для источников, компилятор, макроопределения и так далее. Запуститесь 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 текстовый файл, который перечисляет источники. Можно обновить этот текстовый файл на основе любого нового исходного файла, добавленного к репозиторию исходного кода.

Если необходимо задать целевые и параметры компилятора явным образом, вы не можете разобраться во всех опциях на первом показе. Найти правильную комбинацию опций:

  1. Задайте опции Compiler (-compiler) и Target processor type (-target) в вашем файле опций.

  2. Скомпилируйте код со своим компилятором и зафиксируйте все ошибки компиляции. Затем запуск только часть компиляции анализа Polyspace.

    • В Средстве поиска Ошибки отключите все средства проверки. Задайте -checkers none в файле опций. Смотрите Find defects (-checkers).

    • В Программе автоматического доказательства Кода остановите анализ после компиляции. Задайте -to compile в файле опций. Смотрите Verification level (-to) (Polyspace Code Prover Server).

    Если вы сталкиваетесь с ошибками компиляции, вам придется работать вокруг ошибок с опциями Polyspace. Например, если вы видите ошибку компиляции потому что макро-_WIN32 задан с параметром компилятора, но Polyspace рассматривает макрос как неопределенный по умолчанию, эмулируйте свой параметр компилятора с опцией Polyspace -D _WIN32. Смотрите Цель и Компилятор, Макросы и Параметры среды для целевых и параметров компилятора.

Если вы фиксируете все ошибки компиляции с аналитическими опциями Polyspace, ваш файл опций подготовлен с правильным набором опций Polyspace для анализа.

Если у вас есть установка десктопных решений, Polyspace Bug Finder™ и/или Polyspace Code Prover™, можно выполнить пробные прогоны в пользовательском интерфейсе десктопных решений. Можно затем сгенерировать файл опций от настройки, заданной в пользовательском интерфейсе. Пользовательский интерфейс обеспечивает различные функции, такие как:

  • Ассистент компиляции, который предлагает обходные решения для некоторых ошибок компиляции,

  • Автоматическая генерация XML-файла для ограничительной спецификации,

  • Контекстно-зависимая справка для опций,

Смотрите конфигурируют аналитические опции Polyspace в пользовательском интерфейсе и генерируют скрипты.

Опции, связанные с анализом Polyspace

Некоторые опции, связанные с анализом Polyspace:

Средство поиска ошибки

Программа автоматического доказательства кода

Средства проверки и другие опции, связанные с анализом 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 рассматривается. Если вы хотите заменить предыдущие случаи опции, используйте файл дополнительных опций со своими переопределениями. Добавьте этот файл опций в конец аналитической команды.

Смотрите также

|

Похожие темы