Запуск анализа из DOS или UNIX® командное окно, используйте команду polyspace-bug-finder
или polyspace-code-prover
далее следуют другие опции, которые вы хотите использовать. См. также:
Чтобы сохранить полный путь к командам, добавьте путь
на polyspaceroot
\ polyspace\binPath
окружение в операционной системе. Здесь,
является папкой установки Polyspace, например polyspaceroot
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-code-prover -help
Вместо того, чтобы задавать параметры непосредственно, можно сохранить опции в текстовом файле и использовать текстовый файл каждый раз, когда вы запускаете анализ.
Создайте файл опций с именем 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
Запустите Polyspace, используя опции в файл listofoptions.txt
.
polyspace-code-prover -options-file listofoptions.txt
См. также -options-file
.
Если для создания исходного кода используется команда build (make-файл), можно собрать источники и опции компилятора из команды build. Проследите свою команду build, чтобы сгенерировать текстовый файл с необходимыми опциями Polyspace.
Составьте список опций Polyspace с помощью инструмента строения.
polyspace-configure -output-options-file \ myOptions buildCommand
buildCommand
является ли команда, которую вы используете для создания исходного кода, например make -B
.См. также polyspace-configure
.
Запустите Polyspace, используя опции, считанные из вашей сборки.
polyspace-bug-finder -options-file myOptions \ -results-dir myResults
В дополнение к опциям, собранным из команды build, можно добавить дополнительные опции, например, чтобы задать проверки дефектов. Можно добавить эти опции к файлу опций, добавить их непосредственно в командной строке или добавить их через второй файл опций (используя другой -options-file
флаг).
Откройте результаты в пользовательском интерфейсе Polyspace.
polyspace-bug-finder myResults
polyspace-bug-finder
| polyspace-code-prover
| polyspace-configure