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

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

Если вы не создаете проект Polyspace из существующих технических требований, таких как команда сборки при подготовке проекта, вам придется выполнить несколько пробных прогонов сначала. В этих пробных прогонах, если вы сталкиваетесь с ошибками компиляции или неконтролируемым кодом, вам придется изменить вашу аналитическую настройку. Это - более легкое выполнение этой начальной настройки в пользовательском интерфейсе десктопных решений. Пользовательский интерфейс обеспечивает различные функции, такие как:

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

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

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

Предпосылки

У вас должна быть по крайней мере одна лицензия Polyspace Bug Finder и/или Polyspace Code Prover, чтобы открыть пользовательский интерфейс Polyspace и сконфигурировать опции.

После генерации скриптов можно запустить анализ с помощью любого десктопные решения (Polyspace Bug Finder и Polyspace Code Prover) или серверные продукты (Polyspace Bug Finder Server™ и/или Polyspace Code Prover Server).

Сгенерируйте скрипты от настройки

В этом примере показано, как сгенерировать скрипт от настройки Средства поиска Ошибки. Те же шаги применяются к настройке Программы автоматического доказательства Кода.

  1. Добавьте исходные файлы в новый проект в пользовательском интерфейсе Polyspace.

    Перейдите к polyspaceroot\polyspace\bin, где polyspaceroot папка установки Polyspace, например, C:\Program Files\Polyspace\R2020a. Откройте пользовательский интерфейс Polyspace с помощью polyspace исполняемый файл и создает новый проект.

    Смотрите добавляют исходные файлы для анализа в пользовательском интерфейсе Polyspace (Polyspace Code Prover).

  2. Задайте аналитические опции на панели Configuration в проекте Polyspace. Чтобы открыть эту панель, в браузере проекта, кликают по узлу настройки в вашем проекте Polyspace.

    Смотрите задают аналитические опции Polyspace (Polyspace Code Prover).

  3. Запустите анализ. На основе ошибок компиляции и результатов анализа, измените опции по мере необходимости.

    Смотрите запущенный анализ Polyspace рабочего стола (Polyspace Code Prover).

  4. Если ваши аналитические опции установлены, генерируют скрипт из проекта (.psprj файл).

    Сгенерировать скрипт из демонстрационного проекта, Bug_Finder_Example:

    1. Загрузите проект. Выберите Help> Examples> Bug_Finder_Example.psprj. Копия этого проекта загружается в Examples папка в вашей рабочей области по умолчанию. Чтобы найти местоположение проекта, установите свой курсор на название проекта в панели Project Browser.

    2. Перейдите к местоположению проекта и войдите:

      polyspace -generate-launching-script-for Bug_Finder_Example.psprj -bug-finder

      Чтобы сгенерировать скрипты Программы автоматического доказательства Кода, используйте ту же команду без -bug-finder опция.

      Если проект будет иметь больше чем один модуль (больше чем с одной настройкой в каждом модуле), опции от в настоящее время активной настройки в в настоящее время активном модуле будут извлечены в скрипте.

Эти файлы сгенерированы для сценариев анализа:

  • source_command.txt: Исходные файлы списков. Этот файл может быть предоставлен в качестве аргумента -sources-list-file опция.

  • options_command.txt: Аналитические опции списков. Этот файл может быть предоставлен в качестве аргумента -options-file опция.

  • launchingCommand.bat или launchingCommand.sh, В зависимости от вашей операционной системы. Файл использует polyspace-bug-finder или polyspace-code-prover исполняемый файл, чтобы запустить анализ. Анализ работает на исходных файлах, перечисленных в source_command.txt и использует опции, перечисленные в options_command.txt.

Запустите анализ со сгенерированными скриптами

После конфигурирования вашего анализа и генерации скриптов, можно использовать сгенерированные файлы, чтобы автоматизировать последующий анализ. Можно автоматизировать последующий анализ с помощью или десктопных решений или серверных продуктов.

Автоматизировать анализ Средства поиска Ошибки с десктопным решением, Polyspace Bug Finder:

  1. Сгенерируйте скрипты, как упомянуто в предыдущем разделе.

  2. Выполните скрипт launchingCommand.bat или launchingCommand.sh в периодических интервалах или на основе предопределенных триггеров.

Автоматизировать анализ Средства поиска Ошибки с серверным продуктом, Polyspace Bug Finder Server:

  1. После определения опций в пользовательском интерфейсе и прежде, чем сгенерировать скрипты, переместите проект Polyspace (.psprj файл) к серверу, куда серверный продукт запускается.

  2. Сгенерируйте скрипты, как упомянуто в предыдущем разделе.

    Скрипты относятся к исполняемому файлу серверного продукта вместо десктопных решений.

  3. Выполните скрипт launchingCommand.bat или launchingCommand.sh в периодических интервалах или на основе предопределенных триггеров.

В качестве альтернативы можно изменить скрипт, сгенерированный для десктопного решения так, чтобы серверный продукт был выполнен. Скрипт относится к пути к исполняемому файлу десктопного решения, например:

"C:\Program Files\Polyspace\R2020a\polyspace\bin\polyspace-code-prover.exe"
Замените это на путь к исполняемому файлу серверного продукта, например:
"C:\Program Files\Polyspace Server\R2020a\polyspace\bin\polyspace-code-prover-server.exe"

Иногда, вы можете хотеть заменить некоторые опции в файле опций. Например, опция, чтобы задать папку результатов является hardcoded в скрипте. Можно удалить эту опцию или заменить ее при запуске скриптов:

launchingCommand -results-dir newResultsFolder
где newResultsFolder новая папка результатов. Эта папка может даже быть динамически сгенерирована для каждого запуска.

Если вы заменяете несколько опций в options_command.txt, можно сохранить переопределения во втором файле опций. Измените скрипт launchingCommand.bat или launchingCommand.sh так, чтобы использовались оба файла опций. Скрипт использует опцию -options-file использовать файл опций, например:

-options-file options_command.txt
Если вы помещаете свои переопределения опции во второй файл опций overrides.txt, измените скрипт, чтобы добавить второй -options-file опция:
-options-file options_command.txt -options-file overrides.txt

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

Похожие темы