Exponenta Banner
exponenta event banner

polyspace-code-prover

(DOS/UNIX) Запуск проверки программы проверки кода из Windows, Linux или другой командной строки

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

Синтаксис

polyspace-code-prover [ПАРАМЕТРЫ]
polyspace-code-prover -sources sourceFiles [ПАРАМЕТРЫ]
polyspace-code-prover -sources-list-file listOfSources [ПАРАМЕТРЫ]
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. Чтобы запустить этот пример, замените 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

Для повторного запуска проверки необходимо повторно запустить ее из командной строки.

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

Сохранить этот текст в текстовый файл с именем myOptsFile.txt.

# Polyspace analysis options 
-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
-temporal-exclusions-file polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources\temporal_exclusions.txt
-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++, разделенные запятыми, указаны как строка. Если файлы находятся не в текущей папке (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"

См. также

Темы

Представлен в R2013b

Документация по программе проверки кода Polyspace

Поддержка