Создайте аналитическую настройку Polyspace из команды сборки

Чтобы запустить Polyspace® на сервере во время непрерывного интегрирования, необходимо сконфигурировать все аналитические опции заранее так, чтобы анализ завершился без ошибок. Эти опции должны быть обновлены по мере необходимости, чтобы не отставать от новых представлений кода. Если вы используете существующие артефакты, такие как команда сборки (make-файл), чтобы создать новые представления кода, можно снова использовать команду сборки, чтобы сконфигурировать анализ Polyspace и остаться в курсе с новыми представлениями. С polyspace-configure команда, можно контролировать выполнение команды сборки и создать файл опций для анализа с Polyspace.

Эта тема показывает простой пример, иллюстрирующий, как создать файл опций из команды сборки и использовать файл для последующего анализа. Тема использует make-файл Linux® и компилятор GCC, но можно адаптировать команды к другим операционным системам, таким как Windows® и другие компиляторы, такие как Microsoft® Visual Studio®.

  1. Покров демонстрационные исходные файлы от polyspaceserverroot\polyspace\examples\cxx\Bug_Finder_Example\sources к папке с полномочиями записи. Здесь, polyspaceserverroot корневая папка установки серверных продуктов Polyspace, например, C:\Program Files\Polyspace Server\R2019a.

  2. Создайте простой make-файл, который компилирует демонстрационные исходные файлы. Сохраните make-файл в той же папке как исходные файлы.

    Например, создайте файл с именем makefile и добавьте это содержимое:

    CC := gcc
    SOURCES := $(wildcard *.c)
    
    all: $(CC) -c $(SOURCES)

    Проверяйте, что make-файл создает исходные файлы успешно. Откройте терминал команды, перейдите к папке (использующий cd) и войдите:

    make

    make команда должна завершить выполнение без ошибок.

  3. Проследите команду сборки с polyspace-configure и создайте файл опций compile_opts.

    polyspace-configure -output-options-file compile_opts make

  4. Создайте второй файл опций с дополнительными опциями. Например, создайте файл run_opts с этим содержимым:

    -checkers numerical
    -report-template BugFinder
    -output-format pdf

    Опции запускают все числовые средства проверки в Средстве поиска Ошибки, и создает отчет PDF после анализа с помощью BugFinder шаблон.

  5. Запустите анализ Средства поиска Ошибки с этими двумя файлами опций: 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.

Смотрите также

|

Похожие темы