Запуск анализа Polyspace из командной строки

Запуск анализа из DOS или UNIX® командное окно, используйте команду polyspace-bug-finder или polyspace-code-prover далее следуют другие опции, которые вы хотите использовать. См. также:

Чтобы сохранить полный путь к командам, добавьте путь polyspaceroot\ polyspace\bin на Path окружение в операционной системе. Здесь, polyspaceroot является папкой установки Polyspace, например C:\Program Files\Polyspace\R2021a. См. также Папка установки.

Задайте источники и опции анализа непосредственно

В Windows®, Linux® или Mac OS X в командной строке, добавьте источники и опции анализа к polyspace-bug-finder или polyspace-code-prover команда.

Для образца:

  • Чтобы задать источники, используйте -sources опция, за которой следует разделенный запятыми список источников.

    polyspace-bug-finder -sources C:\mySource\myFile1.c,C:\mySource\myFile2.c

    Если ваша текущая папка содержит sources подпапку с исходными файлами можно опустить -sources флаг. Анализ рассматривает файлы в sources и все подпапки в sources.

  • Чтобы задать целевой процессор, используйте -target опция. Например, чтобы задать m68k процессор для вашего исходного файла file.c, используйте команду:

    polyspace-bug-finder -sources "file.c" -lang c -target m68k
  • Проверить на нарушение MISRA C® правила, используйте -misra2 опция. Например, чтобы проверить только необходимые правила MISRA C в вашем исходном файле file.c, используйте команду:

    polyspace-bug-finder -sources "file.c" -misra2 required-rules
  • Чтобы задать папку результатов, используйте опцию -results-dir.

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

Полный список опций анализа см. в:

Для полного списка опций введите в командной строке следующее:

polyspace-bug-finder -help

Укажите источники и опции анализа в текстовом файле

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

  1. Создайте файл опций с именем listofoptions.txt с вашими опциями. Для примера:

    #These are the options for MyCodeProverProject
    -lang c
    -prog MyCodeProverProject
    -author jsmith
    -sources "mymain.c,funAlgebra.c,funGeometry.c"
    -target x86_64
    -compiler generic
    -dos
    -misra2 required-rules
    -do-not-generate-results-for all-headers
    -main-generator
    -results-dir C:\Polyspace\MyCodeProverProject

  2. Запустите Polyspace, используя опции в файл listofoptions.txt.

    polyspace-code-prover -options-file listofoptions.txt

См. также -options-file.

Создайте файл опций из системы сборки

Если для создания исходного кода используется команда build (make-файл), можно собрать источники и опции компилятора из команды build. Проследите свою команду build, чтобы сгенерировать текстовый файл с необходимыми опциями Polyspace.

  1. Составьте список опций Polyspace с помощью инструмента строения.

    polyspace-configure -output-options-file \
            myOptions buildCommand
    где buildCommand является ли команда, которую вы используете для создания исходного кода, например make -B.

    См. также polyspace-configure.

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

    polyspace-bug-finder -options-file myOptions \
            -results-dir myResults
    

    В дополнение к опциям, собранным из команды build, можно добавить дополнительные опции, например, чтобы задать проверки дефектов. Можно добавить эти опции к файлу опций, добавить их непосредственно в командной строке или добавить их через второй файл опций (используя другой -options-file флаг).

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

    polyspace-bug-finder myResults

См. также

| | (Polyspace Code Prover)

Похожие темы

Внешние веб-сайты