Exponenta Banner

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

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

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

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

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

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

  • Чтобы запустить анализ, установите один экземпляр продукта Polyspace Code Prover Server.

  • Чтобы загрузить результаты, настройте компоненты, требуемые размещать веб-интерфейс Polyspace Code Prover Access.

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

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

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

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

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

  2. Войдите:

    polyspace-code-prover-server -help

Необходимо видеть, что список опций допускал анализ Программы автоматического доказательства Кода.

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

  1. Перейдите снова к polyspaceserverroot\polyspace\bin.

  2. Войдите:

    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 команда.

  3. В веб-браузере откройте этот URL:

    https://hostName:portNumber/metrics/index.html
    Здесь, hostName и portNumber имя хоста и номер порта от предыдущего шага.

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

Запустите программу автоматического доказательства кода на файлах примера

Чтобы запустить Программу автоматического доказательства Кода, в вашей операционной системе, открывают командное окно.

  1. Чтобы запустить анализ Программы автоматического доказательства Кода, используйте polyspace-code-prover-server команда.

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

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

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

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

  2. Войдите:

    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 Access. Можно также получить доступ к документации с помощью кнопки в верхнем правом углу интерфейса Polyspace Access.

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

  • -sources: Задайте разделенные от запятой исходные файлы.

  • -I: Задайте путь, чтобы включать папку. Используйте -I отметьте каждый раз, когда вы хотите добавить, что отдельное включает папку.

  • -results-dir: Задайте путь к папке, где результаты Polyspace Code Prover будут сохранены.

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

  • Verify module or library (-main-generator): Укажите что main функция должна быть сгенерирована если не найденный в исходных файлах

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

polyspace-code-prover-server -doc

Демонстрационные скрипты для анализа программы автоматического доказательства кода серверов

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

Демонстрационный пакетный файл 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 Code Prover).

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

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

  1. Извлеките опции Polyspace из своей команды сборки.

    Например, если вы используете make-файлы, чтобы создать ваш исходный код, можно извлечь аналитические опции из make-файла.

    polyspace-configure -output-options-file compile_opts make

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

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

    polyspace-code-prover-server -options-file compile_opts -options-file run_opts

    Смотрите готовят скрипты к анализу Polyspace.

  3. Загрузите результаты на 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.

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

    Смотрите отправляют уведомления по электронной почте результатами Polyspace Code Prover.

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

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

|

Похожие темы

Документация Polyspace Code Prover Server

Поддержка