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