Чтобы запустить Polyspace® на сервере во время непрерывного интегрирования, необходимо сконфигурировать все аналитические опции заранее так, чтобы анализ завершился без ошибок. Эти опции должны быть обновлены по мере необходимости, чтобы не отставать от новых представлений кода. Если вы используете существующие артефакты, такие как команда сборки (make-файл), чтобы создать новые представления кода, можно снова использовать команду сборки, чтобы сконфигурировать анализ Polyspace и остаться в курсе с новыми представлениями. С polyspace-configure
команда, можно контролировать выполнение команды сборки и создать файл опций для анализа с Polyspace.
Эта тема показывает простой пример, иллюстрирующий, как создать файл опций из команды сборки и использовать файл в последующем анализе. Тема использует make-файл Linux® и компилятор GCC, но можно адаптировать команды к другим операционным системам, таким как Windows® и другие компиляторы, такие как Microsoft® Visual Studio®.
Покров демонстрационные исходные файлы от
к папке с полномочиями записи. Здесь, polyspaceserverroot
\polyspace\examples\cxx\Bug_Finder_Example\sources
корневая папка установки серверных продуктов Polyspace, например, polyspaceserverroot
C:\Program Files\Polyspace Server\R2019a
.
Создайте простой make-файл, который компилирует демонстрационные исходные файлы. Сохраните make-файл в той же папке как исходные файлы.
Например, создайте файл с именем makefile
и добавьте это содержимое:
CC := gcc SOURCES := $(wildcard *.c) all: $(CC) -c $(SOURCES) |
Проверяйте, что make-файл создает исходные файлы успешно. Откройте терминал команды, перейдите к папке (использующий cd
) и войдите:
make |
make
команда должна завершить выполнение без ошибок.
Проследите команду сборки с polyspace-configure
и создайте файл опций compile_opts
.
polyspace-configure -output-options-file compile_opts make |
Создайте второй файл опций с дополнительными опциями. Например, создайте файл run_opts
с этим содержимым:
-checkers numerical -report-template BugFinder -output-format pdf |
Опции запускают все числовые средства проверки в Средстве поиска Ошибки, и создает отчет PDF после анализа с помощью BugFinder
шаблон.
Запустите анализ Средства поиска Ошибки с этими двумя файлами опций: compile_opts
созданный из вашей команды сборки и run_opts
созданный вручную.
polyspace-bug-finder-server -options-file compile_opts -options-file run_opts |
Анализ должен завершиться без ошибок. Можно открыть результаты в пользовательском интерфейсе Polyspace или загрузить результаты на Polyspace доступ к веб-интерфейсу (использующий polyspace-access
команда).
Чтобы запустить Программу автоматического доказательства Кода вместо Средства поиска Ошибки, используйте polyspace-code-prover-server
команда вместо polyspace-bug-finder-server
команда.
Можно запустить подобный анализ с помощью скриптов MATLAB. Замените polyspace-bug-finder-server
с функциональным polyspaceBugFinderServer
и polyspace-configure
с функциональным polyspaceConfigure
.
polyspace-code-prover-server
| polyspace-configure