Exponenta Banner

polyspace-code-prover-server

(DOS/UNIX) Запуск верификация Code Prover на сервере от Windows, Linux или другой командной строки

свернуть все на странице

Синтаксис

polyspace-code-prover-server
polyspace-code-prover-server -sources sourceFiles [OPTIONS]
polyspace-code-prover-server -sources-list-file listOfSources [OPTIONS]
polyspace-code-prover-server -options-file optFile
polyspace-code-prover-server -h[elp]

Описание

polyspace-code-prover-server [OPTIONS] запускает верификацию Code Prover на сервере, если ваша текущая папка содержит sources подпапка с исходными файлами (.c или .cxx файлы). Верификация рассматривает файлы в sources и все подпапки под sources. Можно настроить верификацию с дополнительными опциями.

пример

polyspace-code-prover-server -sources sourceFiles [OPTIONS] запускает верификацию Code Prover на сервере на исходном файле (файлах) sourceFiles. Можно настроить верификацию с дополнительными опциями.

polyspace-code-prover-server -sources-list-file listOfSources [OPTIONS] запускает верификацию Code Prover на сервере на исходных файлах, перечисленных в текстовом файле listOfSources. Можно настроить верификацию с дополнительными опциями.

пример

polyspace-code-prover-server -options-file optFile запускает верификацию Code Prover на сервере с опциями, заданными в файле опции.

polyspace-code-prover-server -h[elp] перечисляет сводные данные возможных опций анализа.

Примеры

свернуть все

Запустите верификацию Code Prover путем определения опций анализа в самой команде. Этот пример использует исходные файлы из демонстрационного примера Polyspace Code Prover. Чтобы запустить этот пример, замените polyspaceserverroot с путем к вашему Polyspace® Установка сервера, например, C:\Program Files\Polyspace Server\R2019a.

Запустите верификацию на numerical.c и programming.c, проверка императивные нормы MISRA C:2012 и использование параметров компилятора GNU 4.7. Эта команда в качестве примера разделена ^ символы для удобочитаемости. На практике можно поместить все команды на одну линию.

polyspaceserverroot\polyspace\bin\polyspace-code-prover-server -lang C^
 -sources polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c,^
 -I polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources\^
 -compiler generic -misra3 mandatory^
 -author jlittle -prog myProject -results-dir C:\Polyspace_Workspace\Results\

После анализа можно загрузить результаты на интерфейс Polyspace Code Prover™ Access™ для анализа. См.:

Запустите верификацию при помощи файла опций, чтобы задать ваши исходные файлы и опции анализа. Чтобы запустить этот пример, замените polyspaceserverroot с путем к вашей установке Сервера Polyspace, например, C:\Program Files\Polyspace Server\R2019a.

Сохраните этот текст к текстовому файлу под названием myOptsFile.txt.

# Polyspace analysis options 
-I polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources
-verif-version 1.0
-sources-list-file polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources\*.c
-lang C
-target i386
-compiler generic
-dos
-do-not-generate-results-for all-headers
-misra3 mandatory-required
-entry-points proc1,proc2,server1,server2,tregulate
-critical-section-begin Begin_CS:Cs10
-critical-section-end End_CS:Cs10
-temporal-exclusions-file polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt
-float-rounding-mode to-nearest
-scalar-overflows-checks signed
-scalar-overflows-behavior truncate-on-error
-uncalled-function-checks none
-check-subnormal allow
-O2
-to Software Safety Analysis level 2
-context-sensitivity-auto
-path-sensitivity-delta 0
-author jlittle 
-prog myProject 
-results-dir C:\Polyspace_Workspace\Results\

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

polyspaceserverroot\polyspace\bin\polyspace-code-prover-server -options-file myOptsFile.txt

После анализа можно загрузить результаты на интерфейс Polyspace Code Prover Access для анализа. См.:

Входные параметры

свернуть все

Разделенный от запятой исходный файл C или C++ называет в виде строки. Если файлы не находятся в текущей папке (pwd), sourceFiles должен включать полный или относительный путь. Чтобы избежать ошибок из-за путей с пробелами, добавьте, заключает в кавычки " " вокруг пути. Для получения дополнительной информации смотрите -sources.

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

Пример: myFile.c, "C:\mySources\myFile1.c,C:\mySources\myFile2.c"

Текстовый файл, который перечисляет имя C или файлов C++ в виде строки. Если файлы не находятся в текущей папке (pwd), listOfSources должен включать полный или относительный путь. Чтобы избежать ошибок из-за путей с пробелами, добавьте, заключает в кавычки " " вокруг пути. Для получения дополнительной информации смотрите -sources-list-file.

Пример: filename.txt, "C:\ps_analysis\source_files.txt"

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

Пример: -lang C-CPP, -target i386

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

Пример: opts.txt, "C:\ps_analysis\options.txt"

Советы

Если при запуске команду как часть скрипта, проверяйте статус выхода, чтобы подтвердить успешный анализ. Команда возвращает нуль согласно успешному анализу. Ненулевое возвращаемое значение означает, что не пройдено анализ и не был завершен. Например, если анализируемый файл не компилирует, команда возвращает ненулевое значение. Если некоторые файлы не компилируют, когда вы анализируете несколько файлов, команда завершает анализ файлов, которые действительно компилируют, и возвращает нуль. Возможно остановить анализ, если файл не компилирует. Смотрите Stop analysis if a file does not compile (-stop-if-compile-error).

После выполнения команды можно проверять %ERRORLEVEL% переменная в командной строке Windows, чтобы подтвердить успешный анализ.

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

Темы

Введенный в R2019a

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

Поддержка