Exponenta Banner

-generate-launching-script-for

Извлеките информацию из файла проекта

Синтаксис

-generate-launching-script-for PRJFILE

Описание

-generate-launching-script-for PRJFILE информация об извлечениях из файла проекта PRJFILE (созданный в пользовательском интерфейсе десктопных решений Polyspace®) так, чтобы можно было запустить анализ из командной строки. Для каждого модуля проекта и каждой настройки в каждом модуле, папка создается содержащий следующие файлы::

  • source_command.txt — Список исходных файлов для -sources-list-file опция.

  • options_command.txt — Список аналитических опций для -options-file опция.

  • temporal_exclusions.txt — Список временных исключений, сгенерированных, только если вы задаете Temporally exclusive tasks (-temporal-exclusions-file) опция.

  • .polyspace_conf.psprj — Копия Polyspace файла проекта раньше генерировала файлы сценариев.

  • launchingCommand.sh (UNIX) или launchingCommand.bat (DOS) — сценарий оболочки, который вызывает правильные команды. Скрипт также вызывает любые опции, которые не могут быть даны -options-file команда, такая как -batch или -add-to-results-repository. Можно дать этому дополнительному анализу файла опции как параметры.

Примечание

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

Примеры

Извлеките информацию, чтобы запустить myproject из командной строки. Используйте эту опцию с настольным бинарным polyspace:

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

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

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

    polyspace -generate-launching-script-for myproject.psprj

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

Темы

Документация Polyspace Code Prover
Поддержка