Exponenta Banner
exponenta event banner

Команда Polyspace Code Prover

(DOS/UNIX) Выполнение верификация Программы автоматического доказательства Кода от DOS или командной строки UNIX

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

Синтаксис

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

Описание

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

пример

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

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

пример

polyspace-code-prover -options-file optFile запускает верификацию Программы автоматического доказательства Кода с опциями, заданными в файле опции.

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

Примеры

свернуть все

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

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

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

Откройте результаты.

polyspaceroot\polyspace\bin\polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

Чтобы повторно выполнить верификацию, необходимо повторно выполнить его из командной строки.

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

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

# Options for 
-I polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources
-verif-version 1.0
-sources polyspaceroot\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
-float-rounding-mode to-nearest
-signed-integer-overflows forbid
-unsigned-integer-overflows allow
-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\

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

polyspaceroot\polyspace\bin\polyspace-code-prover -options-file myOptsFile.txt

Откройте результаты.

polyspaceroot\polyspace\bin\polyspace C:\Polyspace_Workspace\Results\ps_results.pscp

Чтобы повторно выполнить верификацию, необходимо повторно выполнить его из командной строки.

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

свернуть все

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

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

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

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

Пример: -sources-list-file filename.txt, -sources-list-file "C:\ps_analysis\source_files.txt"

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

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

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

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

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

Темы

Введенный в R2013b

Документация Polyspace Code Prover
Поддержка