polyspace-configure

(DOS/UNIX) Создает проект Polyspace из вашей системы сборки в командной строке UNIX или DOS

Описание

пример

polyspace-configure buildCommand прослеживает вашу систему сборки и создает проект Polyspace® с информацией, собранной от вашей системы сборки.

пример

polyspace-configure [OPTIONS] buildCommand прослеживает вашу систему сборки и использует -option value изменить операцию по умолчанию polyspace-configure. Задайте модификаторы перед buildCommand, в противном случае они рассматриваются как опции в самой команде сборки.

пример

polyspace-configure [OPTIONS] -compilation-database jsonFile создает проект Polyspace с информацией, собранной из файла базы данных компиляции JSON jsonFile то, что вы обеспечиваете. Вы не должны задавать команду сборки или прослеживать вашу систему сборки. Для больше на базах данных компиляции JSON, см. Базу данных Компиляции JSON.

Примеры

свернуть все

В этом примере показано, как создать проект Polyspace, если вы используете команду, делают targetName buildOptions создавать ваш исходный код.

Создайте проект Polyspace, задающий уникальное название проекта. Используйте -B или-W makefileName опция с make так, чтобы все необходимые как условие цели в make-файле были переделаны.

polyspace-configure  -prog myProject \
make -B targetName buildOptions

Откройте проект Polyspace в пользовательском интерфейсе Polyspace.

В этом примере показано, как создать файл опций Polyspace из базы данных компиляции JSON, которую вы генерируете с генератором системы сборки CMake. CMake генерирует инструкции по сборке для инструмента сборки, который вы задаете, такие как Unix Make-файлы для make или файлы проекта для Microsoft® Visual Studio®. CMake поддерживает генерацию базы данных компиляции JSON только для генераторов Make-файла и генератора Ниндзя. Для получения дополнительной информации смотрите генераторы make-файла.

Сгенерируйте базу данных компиляции JSON для своего проекта CMake. Для примера проекта Cmake смотрите polyspaceroot\help\toolbox\bugfinder\examples\compilation_database где polyspaceroot ваша папка установки Polyspace.

Перейдите к корню вашего исходного дерева проекта. Эта папка содержит файл CMakeLists.txt который CMake использует в качестве входа, чтобы сгенерировать инструкции по сборке. Введите эти команды:

mkdir JSON_cdb
cd JSON_cdb
cmake -G "Unix Makefiles" -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../
Последняя команда генерирует make-файл Unix с инструкциями по сборке для make создайте инструмент. Команда также выходной файл compile_commands.json. Это списки файлов компилятор призывает к каждому модулю перевода в вашем проекте.

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

polyspace-configure -compilation-database compile_commands.json \
-output-options-file options.txt
Вы не должны задавать команду сборки и polyspace-configure не прослеживает вашу сборку. Polyspace извлекает информацию о вашей системе сборки от базы данных компиляции JSON.

Передайте файл опций Polyspace, чтобы запустить анализ, например:

polyspace-bug-finder -options-file options.txt

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

Проследите свою систему сборки, не создавая проект Polyspace путем определения опции -no-project. Чтобы гарантировать, что все необходимые как условие цели в вашем make-файле переделаны, используйте соответствующий make создайте опцию команды, например, -B.

polyspace-configure -no-project make -B

polyspace-configure хранит информацию кэша и трассировку сборки в местоположениях по умолчанию в текущей папке. Чтобы хранить информацию кэша и трассировку сборки в другом месте, задайте опции -cache-path и -build-trace.

Сгенерируйте проекты Polyspace при помощи трассировочной информации сборки от предыдущего шага. Задайте название проекта и используйте -include-sources или -exclude-sources опция, чтобы выбрать, который файлы включать для каждого проекта.

polyspace-configure -no-build -prog myProject \
-include-sources "glob_pattern"

glob_pattern шаблон шарика, который соответствует папкам или файлам, вы просачиваетесь или из вашего проекта. Гарантировать интерпретатор не расширяет шаблоны шарика, которые вы передаете polyspace-configure, заключите их в двойные кавычки. Для получения дополнительной информации о поддерживаемом синтаксисе для шаблонов шарика смотрите, что полипробел - конфигурирует Синтаксис Выбора Исходных файлов.

Если вы задали опции -build-trace и -cache-path на предыдущем шаге задайте их снова.

Удалите папка кэша и файл трассировки.

rm -r polyspace_configure_cache polyspace_configure_built_trace
 
Если вы использовали опции -build-trace и -cache-path, используйте пути и имена файлов из тех опций.

В этом примере показано, как запустить анализ Polyspace, если вы используете команду, делают targetName buildOptions создавать ваш исходный код. В этом примере вы используете polyspace-configure прослеживать вашу систему сборки, но не создавать проект Polyspace. Вместо этого вы создаете файл опций, который можно использовать, чтобы запустить анализ Polyspace от командной строки.

Создайте файл опций Polyspace, задающий -output-options-file команда. Используйте -B или-W makefileName опция с make так, чтобы были переделаны все необходимые как условие цели в make-файле.

polyspace-configure -output-options-file\
 myOptions make -B targetName buildOptions

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

polyspace-bug-finder -options-file myOptions

Входные параметры

свернуть все

Создайте команду, заданную точно так же, как вы используете, чтобы создать ваш исходный код.

Пример: make -B, сделайте-W makefileName

Основные опции

ОпцияАргументОписание
-progНазвание проекта

Название проекта, которое появляется в пользовательском интерфейсе Polyspace. Значением по умолчанию является polyspace.

Если вы не используете опцию -output-project, -prog аргумент также устанавливает название проекта.

Пример: -prog myProject создает проект, который имеет имя myProject в пользовательском интерфейсе. Если вы не используете опцию -output-project, названием проекта является также myProject.psrprj.

-authorИмя автора

Имя автора проекта.

Пример: -author jsmith

-output-projectPath

Имя файла проекта и местоположение для сохранения проекта. Значением по умолчанию является файл polyspace.psprj в текущей папке.

Пример: -output-project ../myProjects/project1 создает проект project1.psprj в папке с относительным путем ../myProjects/.

-output-options-fileFileName

Опция, чтобы создать файл опций анализа Polyspace. Используйте этот файл для анализа командной строки с помощью одной из этих команд:

  • polyspace-bug-finder

  • polyspace-code-prover

  • polyspace-bug-finder-server

  • polyspace-code-prover-server

  • polyspace-bug-finder-access

-allow-build-error'none'

Опция, чтобы создать проект Polyspace, даже если ошибка происходит в процессе сборки.

Если ошибка происходит, журнал трассировки сборки показывает следующее сообщение:

polyspace-configure (polyspaceConfigure) 
   ERROR: build command 
   command_name fail [status=status_value]
command_name название команды сборки, которое вы используете и status_value ненулевой статус выхода или ошибочный уровень, который указывает, какая ошибка произошла в вашем процессе сборки.

Эта опция проигнорирована, когда вы используете -compilation-database.

-allow-overwrite'none'

Опция, чтобы перезаписать проект с тем же именем, если это существует.

По умолчанию, polyspace-configure (polyspaceConfigure) выдает ошибку, если проект с тем же именем уже существует в выходной папке. Используйте эту опцию, чтобы перезаписать проект.

-no-console-output

-silent (значение по умолчанию)

-verbose

'none'

Опция, чтобы подавить или отобразить дополнительные сообщения от выполнения polyspace-configure (polyspaceConfigure).

  • -no-console-output – Подавите все выходные параметры включая ошибки и предупреждения.

  • -silent (значение по умолчанию) – Показывает только ошибки и предупреждения.

  • -verbose – Покажите все сообщения.

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

Эти опции проигнорированы, если они используются в сочетании с -easy-debug.

-help'none'

Опция, чтобы отобразить полный список polyspace-configure (polyspaceConfigure) команды

-debug'none'

Опция, чтобы сохранить отладочную информацию для использования технической поддержкой MathWorks®.

Эта опция была заменена опцией -easy-debug.

-easy-debugPath

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

После polyspace-configure (polyspaceConfigure) запуститесь, обеспеченный путь содержит заархивированный файл, заканчивающийся pscfg-output.zip. Если запуску не удается создать полный проект Polyspace или файл опций, отправьте этот заархивированный файл MathWorks Technical Support для дальнейшей отладки. Заархивированный файл не содержит исходные файлы, прослеженные в сборке. См. также Ошибки в Создании Проекта от Систем сборки.

Опции, чтобы создать несколько модулей

Эти опции не совместимы с -compilation-database.

ОпцияАргументОписание
-module'none'

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

Можно только создать отдельные файлы опций для различных двоичных файлов. Вы не можете создать несколько модулей в проекте Polyspace (для выполнения в пользовательском интерфейсе Polyspace).

Используйте эту опцию только для систем сборки, которые используют GNU® и Визуальный C ++® компиляторы.

См. также Строят Анализ Polyspace из модулей при помощи Команды Сборки.

-output-options-pathПуть

Местоположение, где сгенерированные файлы опций сохранены. Используйте эту опцию вместе с опцией -module.

Файлы опций называют после того, как двоичные файлы создали в системе сборки.

Расширенные настройки

ОпцияАргументОписание
-compilation-databaseПуть и имя файла

Местоположение и имя базы данных компиляции JSON (JSON CDB) файл. Вы генерируете этот файл от своей системы сборки, например, при помощи флага -DCMAKE_EXPORT_COMPILE_COMMANDS=1 с cmake. Файл содержит призывы компилятора ко всем модулям перевода в вас проекты. Для получения дополнительной информации см. Базу данных Компиляции JSON. polyspace-configure использует содержимое этого файла, чтобы получить информацию о вашей системе сборки. Извлеченные пути к компилятору в JSON CDB должны быть доступными от пути, куда вы запускаете polyspace-configure.

Вы не задаете команду сборки, когда вы используете эту опцию.

Системы сборки и компиляторы поддерживают генерацию JSON CDB:

  • CMake

  • Bazel

  • Лязг

  • Ниндзя

  • Qbs

  • WAF

Эта опция не совместима с -no-project и с опциями, чтобы создать несколько модулей.

Опции управления кэшем, -allow-build-error, и -no-build проигнорированы, когда вы используете эту опцию.

-compiler-configПуть и имя файла

Местоположение и имя конфигурационного файла компилятора.

Файл должен быть в определенном формате. Для руководства смотрите существующие конфигурационные файлы в polyspaceroot\polyspace\configure\compiler_configuration\. Для получения информации о содержимом файла см. Компилятор, Не Поддержанный для Создания Проекта от Систем сборки.

Пример: -compiler-configuration myCompiler.xml

-no-project'none'

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

Используйте эту опцию, чтобы сохранить вашу трассировочную информацию сборки для более позднего запуска polyspace-configure (polyspaceConfigure) с -no-build опция.

Эта опция не совместима с -compilation-database.

-no-build'none'

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

Чтобы использовать эту опцию, у вас должна быть трассировочная информация сборки, сохраненная от более раннего запуска polyspace-configure (polyspaceConfigure) с -no-project опция.

Если вы используете эту опцию, вы не должны задавать buildCommand аргумент.

Эта опция проигнорирована, когда вы используете -compilation-database.

-no-sources'none'

Опция, чтобы создать файл опций Polyspace, который не содержит технические требования исходного файла.

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

  • Рабочий Polyspace на AUTOSAR-специфичном коде.

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

    -output-options-file options.txt -no-sources
    Вы позже добавляете этот файл опций при извлечении имен исходного файла из технических требований ARXML и выполнении последующего анализа Программы автоматического доказательства Кода с polyspace-autosar (Polyspace Code Prover)
    -extra-options-file options.txt

    См. также Polyspace Запуска на Коде AUTOSAR Используя Команду Сборки (Polyspace Code Prover).

  • Рабочий Polyspace в Eclipse™.

    Ваши исходные файлы уже заданы в вашем проекте Eclipse. При выполнении анализа Polyspace вы хотите задать файл опций, который имеет параметры компиляции только.

-extra-project-optionsОпции, чтобы использовать для последующего анализа Polyspace. Например, "-stubbed-pointers-are-unsafe".

Опции, которые используются для последующего анализа Polyspace.

Если проект Polyspace создается, можно изменить некоторые опции по умолчанию в проекте. В качестве альтернативы можно передать эти опции при трассировке команды сборки. Флаг -extra-project-options позволяет вам передавать дополнительные опции.

Укажите, что несколько опций на пробеле разделили список, например, "-allow-negative-operand-in-shift -stubbed-pointers-are-unsafe".

Предположим, что необходимо установить опцию -stubbed-pointers-are-unsafe для каждого созданного проекта Polyspace. Вместо того, чтобы открыть каждый проект и установить опцию, можно использовать этот флаг при создании проекта Polyspace:

-extra-project-options "-stubbed-pointers-are-unsafe"

Для списка доступных опций см.:

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

-tmp-pathPathМестоположение папки, где временные файлы хранятся.
-build-traceПуть и имя файла

Местоположение и имя файла, где информация о сборке хранится. Значением по умолчанию является ./polyspace_configure_build_trace.log.

Пример: -build-trace ../build_info/trace.log

-include-sources

-exclude-sources

Шаблон шарика

Опция, чтобы задать, который исходные файлы polyspace-configure (polyspaceConfigure) включает в или исключает из, сгенерированный проект. Можно объединить обе опции вместе.

Исходный файл включен, если путь к файлу совпадает с шаблоном шарика, который вы передаете -include-sources.

Исходный файл исключен, если путь к файлу совпадает с шаблоном шарика, который вы передаете -exclude-sources.

-print-included-sources

-print-excluded-sources

'none'

Опция, чтобы распечатать список исходных файлов, что polyspace-configure (polyspaceConfigure) включает в или исключает из, сгенерированный проект. Можно объединить обе опции вместе. Выход отображает полный путь каждого файла на отдельной линии.

Используйте эту опцию, чтобы диагностировать шаблоны шарика, которые вы передаете -include-sources или -exclude-sources. Вы видите, какие файлы совпадают с шаблоном, который вы передаете -include-sources или -exclude-sources.

-compiler-cache-pathПуть к папке

Задайте путь к папке где polyspace-configure ищет или хранит файлы кэша компилятора. Если папка не существует, polyspace-configure создает его.

По умолчанию Polyspace ищет и хранит кэши компилятора под этими путями к папкам:

  • Windows®

    %appdata%\Mathworks\R20xxY\Polyspace

  • Linux®

    ~/.matlab/R20xxY/Polyspace

  • Mac

    ~/Library/Application Support/MathWorks/MATLAB/R20xxY/Polyspace

R20xxY версия выпуска вашего Продукта polyspace, например, R2020b.

-no-compiler-cache'none'

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

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

-reset-compiler-cache-entry'none'Используйте эту опцию, чтобы запросить компилятор для текущей настройки и обновить запись в файле кэша, который соответствует этой настройке. Другие записи настройки компилятора в кэше не обновляются.
-clear-compiler-cache'none'

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

Если вы также задаете команду сборки или -compilation-database, polyspace-configure вычисляет и кэширует конфигурационную информацию компилятора текущего запуска, кроме того, если вы задаете -no-project или -no-compiler-cache.

-import-macro-definitions

none

from-whitelist

from-source-tokens

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

Можно задать:

  • none — Polyspace не запрашивает компилятор для макроопределений. Необходимо обеспечить макроопределения вручную.

  • from-whitelist — Polyspace использует внутренний белый список, чтобы запросить компилятор для макроопределений.

    Polyspace использует белый список по умолчанию, когда вы используете опцию -compilation-database.

  • from-source-tokens (значение по умолчанию, кроме того, если вы используете -compilation-database ) — Polyspace использует каждую лексему неключевого слова в вашем исходном коде, чтобы запросить ваш компилятор для макроопределений.

-options-for-sources-delimiterОтдельный символ

Задайте диафрагму опции, чтобы использовать, когда несколько опций анализа будут сопоставлены с одним исходным файлом с помощью -options-for-sources опция. Как правило, -options-for-sources опция использует точку с запятой в качестве диафрагмы.

См. также -options-for-sources.

Опции управления кэшем

Эти опции, в основном, полезны для отладки. Используйте опции если polyspace-configure (polyspaceConfigure) сбои и MathWorks Technical Support просят, чтобы вы использовали опцию и обеспечили кэшируемые файлы. Запуская R2020a, опция -easy-debug обеспечивает более легкий способ обеспечить отладочную информацию. Смотрите Техническую поддержку Контакта О Проблемах с Рабочим Polyspace.

Эти опции проигнорированы, когда вы используете -compilation-database.

ОпцияАргументОписание

-no-cache

-cache-sources (значение по умолчанию)

-cache-all-text

-cache-all-files

'none'

Опция, чтобы выполнить одно из следующего:

  • -no-cache: Не создают кэш

  • -cache-sources: Текстовые файлы кэша временно создаются во время сборки для дальнейшего использования polyspace-configure (polyspaceConfigure).

  • -cache-all-text: Кэш все текстовые файлы включая источники и заголовки.

  • -cache-all-files: Кэш все файлы включая двоичные файлы.

Как правило, вы кэшируете временные файлы, созданные вашей командой сборки, чтобы отладить проблемы в трассировке команды.

-cache-pathPath

Местоположение папки, где информация о кэше хранится.

При трассировке сборки Visual Studio (devenv.exe), если вы видите ошибку:

path is too long
попытайтесь использовать более короткий путь для этой опции, чтобы работать вокруг ошибки.

Пример: -cache-path ../cache

-keep-cache

-no-keep-cache (значение по умолчанию)

'none'

Опция, чтобы сохранить или очистить информацию о кэше после polyspace-configure (polyspaceConfigure) завершает выполнение.

Если polyspace-configure (polyspaceConfigure) сбои, можно предоставить эту информацию о кэше технической поддержке для отладки целей.

Введенный в R2013b