Для выполнения анализа из окна команд DOS или UNIX ® используйте командуpolyspace-bug-finder или polyspace-code-prover далее следуют другие параметры, которые вы хотите использовать. См. также:
Чтобы сохранить ввод полного пути к командам, добавьте путь polyspaceroot\polyspace\binPath переменная среды в операционной системе. Здесь, polyspacerootC:\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 (makefile), можно собрать исходные данные и параметры компилятора из команды build. Выполните трассировку команды build для создания текстового файла с требуемыми параметрами Polyspace.
Создайте список опций Polyspace с помощью инструмента настройки.
polyspace-configure -output-options-file \
myOptions buildCommandbuildCommand является командой, используемой для построения исходного кода, например, 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