Запустите Polyspace Code Prover на сервере и загрузите результаты на веб-интерфейс

Polyspace^® Code Prover™ Server™ доказывает отсутствие ошибок времени выполнения в коде C/C++, и затем загружает результаты на веб-интерфейс для рассмотрения кода.

Можно запустить Code Prover как часть непрерывного интегрирования. Настройте скрипты, которые запускают анализ Code Prover равномерно или на основе новых представлений кода. Скрипты могут загрузить результаты анализа для анализа в веб-интерфейсе Polyspace и опционально послать электронные письма владельцам исходных файлов с результатами Polyspace. Владельцы могут открыть веб-интерфейс, чтобы рассмотреть только новые результаты от их представления, и затем зафиксировать или выровнять по ширине проблемы.

В типичном проекте или команде, Polyspace Code Prover Server периодически запускается на нескольких серверах тестирования и загружает результаты для анализа. У каждого разработчика и инженера по качеству в команде есть лицензия Polyspace Code Prover Access™, чтобы просмотреть результаты в веб-интерфейсе для расследования и устранения ошибки.

Необходимые условия

Чтобы запустить анализ Code Prover сервера и рассмотреть результаты в веб-интерфейсе Polyspace Code Prover Access, выполните эту одноразовую настройку:

Чтобы запустить анализ, установите один экземпляр продукта Polyspace Code Prover Server.
Чтобы загрузить результаты, настройте компоненты, требуемые размещать веб-интерфейс Polyspace Code Prover Access.
Чтобы просмотреть загруженные результаты, у вас и каждого разработчика, рассматривающего результаты, должна быть лицензия Polyspace Code Prover Access.

Смотрите сервер Polyspace установки и доступ к продуктам.

Проверяйте установку Polyspace

Чтобы проверять, установлен ли Polyspace Code Prover Server:

Откройте командное окно. Перейдите к polyspaceserverroot\polyspace\bin. Здесь, polyspaceserverroot папка установки Polyspace Code Prover Server, например, C:\Program Files\Polyspace Server\R2021b. См. также Папку Установки.
Войдите:
polyspace-code-prover-server -help

Необходимо видеть, что список опций допускал анализ Code Prover.

Чтобы проверять, настраивается ли веб-интерфейс Polyspace для загрузки:

Перейдите снова к polyspaceserverroot\polyspace\bin.
Войдите:
polyspace-access -host hostName -port portNumber -create-project testProject
Здесь, hostName имя сервера, размещающего веб-сервер Polyspace Code Prover Access. Для локально размещенного сервера используйте localhost. portNumberЯ - дополнительный номер порта сервера. Если вы не используете номер порта, 9443 используется.
Если настройка была завершена, проект под названием testProject создается в веб-интерфейсе Polyspace.
Вам предлагают ваш вход в систему и пароль каждый раз, когда вы используете polyspace-access команда. Чтобы постараться не вводить информацию о входе в систему каждый раз, обеспечьте вход в систему и зашифрованную версию вашего пароля с командой. Создать зашифрованный пароль, введите:
polyspace-access -encrypt-password
Введите свой вход в систему и пароль. Скопируйте зашифрованный пароль и предоставьте этому зашифрованному паролю -encrypted-password опция при использовании polyspace-access команда.
В веб-браузере откройте этот URL:
```
https://hostName:portNumber/metrics/index.html
```
Здесь, hostName и portNumber имя хоста и номер порта от предыдущего шага.

В панели Project Explorer на веб-интерфейсе Polyspace необходимо видеть недавно созданный проект testProject.

Запустите Code Prover на файлах примера

Чтобы запустить Code Prover, в вашей операционной системе, открывают командное окно.

Чтобы запустить анализ Code Prover, используйте polyspace-code-prover-server команда.
Чтобы загрузить результаты на веб-интерфейс Polyspace, используйте polyspace-access команда.

Чтобы постараться не вводить полный путь к команде, добавьте путь polyspaceserverroot\polyspace\bin к Path переменная окружения на вашей операционной системе.

Испытайте команды на файлах примера, которым предоставляют вашу установку Polyspace.

Скопируйте демонстрационные исходные файлы с polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources к другой папке, где у вас есть полномочия записи. Перейдите к этой папке в командной строке.

Войдите:

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .
polyspace-access -host hostName -port portNumber -login username -encrypted-password pwd -create-project testProject
polyspace-access -host hostName -port portNumber -login username -encrypted-password pwd -upload . -project myFirstProject -parent-project testProject

Здесь, username ваше имя для входа в систему и pwd зашифрованный пароль, который вы создали ранее. Смотрите Установку Polyspace Проверки.

Обновите веб-интерфейс Polyspace. Вы видите недавно загруженные результаты под testProject папка в панели Project Explorer.

Чтобы видеть результаты в проекте, нажмите Review. Для получения дополнительной информации смотрите, Рассматривают Результаты Polyspace Code Prover в веб-браузере. Можно также получить доступ к документации с помощью кнопки в верхнем правом углу интерфейса Polyspace Access.

Опции используются с polyspace-code-prover-server команда:

-sources: Задайте разделенные от запятой исходные файлы.
-I: Задайте путь, чтобы включать папку. Используйте -I отметьте каждый раз, когда вы хотите добавить, что отдельное включает папку.
-results-dir: Задайте путь к папке, где результаты Polyspace Code Prover будут сохранены.
Обратите внимание на то, что папка результатов очищена и повторно заполнена при каждом запуске. Чтобы избежать случайного удаления файлов во время очистки, вместо того, чтобы использовать существующую папку, которая содержит другие файлы, задают специализированную папку для результатов Polyspace.
Verify module or library (-main-generator): Укажите что main функция должна быть сгенерирована если не найденный в исходных файлах

Для полного списка опций, доступных для анализа Code Prover, см. Полный список Опций анализа Polyspace Code Prover. Открыть документацию Code Prover в браузере документации, введите:

polyspace-code-prover-server -doc

Демонстрационные скрипты для анализа Code Prover серверов

Чтобы запустить анализ, вместо того, чтобы ввести команды в командной строке, можно использовать скрипты. Скрипты могут выполниться каждый раз, когда вы добавляете или изменяете исходные файлы.

Демонстрационный Windows^® пакетный файл показывают ниже. Здесь, путь к установке Polyspace задан в скрипте. Чтобы использовать этот скрипт, замените polyspaceserverroot с путем к вашей установке. Вы, должно быть, уже сгенерировали зашифрованный пароль для использования в скриптах. Смотрите Установку Polyspace Проверки.

echo off
set POLYSPACE_PATH=polyspaceserverroot\polyspace\bin
set LOGIN=-host hostName -port portNumber -login username -encrypted-password pwd
"%POLYSPACE_PATH%\polyspace-code-prover-server" -sources example.c,single_file_analysis.c -I .^
 -main-generator -results-dir .
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -create-project testProject
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -upload . -project myFirstProject -parent-project testProject
pause

Демонстрационный Linux^® сценарий оболочки показывают ниже.

POLYSPACE_PATH=polyspaceserverroot/polyspace/bin
LOGIN=-host hostName -port portNumber -login username -encrypted-password pwd
${POLYSPACE_PATH}/polyspace-code-prover-server -sources example.c,single_file_analysis.c -I .\
 -main-generator -results-dir .
${POLYSPACE_PATH}/polyspace-access $LOGIN -create-project testProject
${POLYSPACE_PATH}/polyspace-access $LOGIN -upload . -project myFirstProject -parent-project testProject

Задайте источники и опции в отдельных файлах из запускающихся скриптов

Вместо того, чтобы перечислить исходные файлы и опции анализа в рамках запускающихся скриптов, можно перечислить их в отдельных текстовых файлах.

Задайте текстовый файл, перечисляющий источники при помощи опции -sources-list-file.
Задайте текстовый файл, перечисляющий опции анализа при помощи опции -options-file.

Путем удаления исходных файлов и технических требований опции анализа из запускающихся скриптов, можно изменить эти технические требования как требуется с новыми представлениями кода при оставлении запускающегося скрипта нетронутым.

Рассмотрите скрипт в предыдущем примере. Можно изменить polyspace-code-prover-server команда, чтобы использовать текстовые файлы с источниками и опции. Вместо:

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .

использование:

polyspace-code-prover-server -sources-list-file sources.txt -options-file polyspace_opts.txt -results-dir .

Здесь:

sources.txt списки исходные файлы:
```
example.c
single_file_analysis.c
```
polyspace_opts.txt перечисляет опции анализа в отдельных линиях:
```
-I .
-main-generator
```

Как правило, ваши исходные файлы заданы в команде сборки (make-файл). Вместо того, чтобы задать исходные файлы непосредственно, можно проследить команду сборки, чтобы создать список исходных технических требований. Смотрите polyspace-configure.

Полный рабочий процесс

В типичном непрерывном рабочем процессе интегрирования вы запускаете скрипт, который выполняет эти шаги:

Извлеките опции Polyspace из своей команды сборки.
Например, если вы используете make-файлы, чтобы создать ваш исходный код, можно извлечь опции анализа из make-файла.
polyspace-configure -output-options-file compile_opts make
Смотрите также:
- polyspace-configure
- Создайте аналитическую настройку Polyspace из команды сборки (make-файл)
Запустите анализ с ранее созданным файлом опций. Добавьте второй файл опций, который содержит остающиеся опции, требуемые для анализа.
polyspace-code-prover-server -options-file compile_opts -options-file run_opts
Смотрите определение нескольких файлов опций.

Загрузите результаты на Polyspace Code Prover Access.

polyspace-access login -upload resultsFolder -project projName -parent-project parentProjName

Здесь, login комбинация опций, требуемых связываться с веб-сервером, который размещает Polyspace Code Prover Access:

-host hostName -port portNumber -login username -encrypted-password pwd

resultsFolder папка, содержащая результаты Polyspace. projName и parentProjName имена проекта и порождают папку, когда они появились бы в веб-интерфейсе Polyspace Code Prover Access.

Опционально, отправьте уведомления по электронной почте разработчикам с новыми результатами их представления кода. Электронная почта содержит прикрепления со ссылками на результаты в веб-интерфейсе Polyspace Code Prover Access.
Смотрите отправляют уведомления по электронной почте результатами Polyspace Code Prover Server.

Смотрите примеры скриптов, выполняющих эти шаги в Демонстрационных Скриптах для Анализа Polyspace с Дженкинсом.

Документация