Exponenta Banner
exponenta event banner

polyspaceCodeProver

Запустите верификацию Polyspace Code Prover из MATLAB

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

Для более легких сценариев запустите анализ Polyspace® с помощью объекта polyspace.Project.

Синтаксис

polyspaceCodeProver
polyspaceCodeProver(projectFile)
polyspaceCodeProver(optsObject)
polyspaceCodeProver(projectFile, '-nodesktop')
polyspaceCodeProver(resultsFile)
polyspaceCodeProver('-results-dir',resultsFolder)
polyspaceCodeProver('-help')
polyspaceCodeProver('-sources',sourceFiles)
polyspaceCodeProver('-sources',sourceFiles,Name,Value)

Описание

polyspaceCodeProver открывает Polyspace Code Prover™.

пример

polyspaceCodeProver(projectFile) открывает файл проекта Polyspace в Polyspace Code Prover.

polyspaceCodeProver(optsObject) запускает верификацию на объекте опций Polyspace в MATLAB®.

polyspaceCodeProver(projectFile, '-nodesktop') запускает верификацию на файле проекта Polyspace в MATLAB. Если у вас есть несколько модулей или настроек, Polyspace запускает активную настройку и активный модуль. Чтобы видеть, какой модуль и настройка активны, откройте проект в интерфейсе Polyspace и ищите полужирный, выбранный модуль и настройку. Чтобы измениться, какой модуль или настройка активны, прежде, чем закрыть интерфейс Polyspace, выбирают модуль и настройку, которую вы хотите проверить.

polyspaceCodeProver(resultsFile) открывается Polyspace приводит файл к Polyspace Code Prover.

пример

polyspaceCodeProver('-results-dir',resultsFolder) открывается Polyspace происходит файл от resultsFolder в Polyspace Code Prover.

polyspaceCodeProver('-help') отображения все опции, которые могут быть предоставлены команде polyspaceCodeProver, чтобы запустить верификацию Polyspace Code Prover.

пример

polyspaceCodeProver('-sources',sourceFiles) запускает верификацию Polyspace Code Prover на исходных файлах, заданных в sourceFiles.

пример

polyspaceCodeProver('-sources',sourceFiles,Name,Value) запускает верификацию Polyspace Code Prover на исходных файлах с дополнительными опциями, заданными одним или несколькими аргументами пары Name,Value.

Примечание

Прежде чем вы запустите Polyspace из MATLAB, необходимо соединить Polyspace и установки MATLAB. Смотрите Интегрируют Polyspace с MATLAB и Simulink.

Примеры

свернуть все

Этот пример показывает, как открыть файл проекта Polyspace с дополнительным .psprj из MATLAB. В этом примере откройте файл проекта Code_Prover_Example.psprj.

Присвойте полный путь к файлу проекта к переменной MATLAB prjFile.

prjFile = fullfile(polyspaceroot, 'polyspace', 'examples', 'cxx', ...
         'Code_Prover_Example', 'Code_Prover_Example.psprj');

Откройте проект.

polyspaceCodeProver(prjFile)

Этот пример показывает, как открыться, Polyspace происходит файл от MATLAB. В этом примере вы открываете файл результатов от папки polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\Module_1\CP_Result.

Присвойте весь путь к папке к переменной MATLAB resFolder.

resFolder = fullfile(polyspaceroot, 'polyspace', 'examples', ...
       'cxx', 'Code_Prover_Example', 'Module_1', 'CP_Result');

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

polyspaceCodeProver('-results-dir',resFolder)

Этот пример показывает, как запустить верификацию Polyspace в объектах использования MATLAB. Для этого примера:

  • Сохраните исходный файл C, source.c, в папке C:\Polyspace_Sources.

  • Сохраните включать файл в папке C:\Polyspace_Includes.

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

opts = polyspace.CodeProverOptions;
opts.Sources = {'C:\Polyspace_Sources\source.c'};
opts.EnvironmentSettings.IncludeFolders = {'C:\Polyspace_Includes'};
opts.ResultsDir = 'C:\Polyspace_Results';

Запустите верификацию и просмотрите результаты.

polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',opts.ResultsDir)

Polyspace работает на файле C:\Polyspace_Sources\source.c и хранит результат в C:\Polyspace_Results.

Этот пример показывает, как запустить верификацию Polyspace на одном исходном файле. Для этого примера:

  • Сохраните исходный файл C, source.c, в папке C:\Polyspace_Sources.

  • Сохраните включать файл в папке C:\Polyspace_Includes.

Запустите анализ и откройте результаты.

polyspaceCodeProver('-sources','C:\Polyspace_Sources\source.c', ...
             '-I','C:\Polyspace_Includes', ...
             '-results-dir','C:\Polyspace_Results')
polyspaceCodeProver('-results-dir','C:\')

Этот пример показывает два различных способа настроить верификацию в MATLAB. Можно настроить столько дополнительных опций, сколько вы хотите путем изменения свойств в объекте опций или при помощи Пар "имя-значение". Вы задаете проверку правил кодирования MISRA C® 2012, исключаете заголовки из кодирования проверки правила и генерируете основное.

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

sourceFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','example.c');
includeFileName = fullfile(polyspaceroot, 'polyspace','examples', 'cxx', 'Code_Prover_Example','sources','include.h');
resFolder1 = fullfile('Polyspace_Results_1');
resFolder2 = fullfile('Polyspace_Results_2');

Проверьте правила кодирования с объектом опций.

opts = polyspace.CodeProverOptions('C');
opts.Sources = {sourceFileName};
opts.EnvironmentSettings.IncludeFolders = {includeFileName};
opts.ResultsDir = resFolder1;
opts.CodingRulesCodeMetrics.MisraC3Subset = 'mandatory';
opts.CodingRulesCodeMetrics.EnableMisraC3 = true;
opts.CodeProverVerification.EnableMain = true;
opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers';
polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',resFolder1);

Проверьте правила кодирования с опциями DOS/UNIX.

polyspaceCodeProver('-sources',sourceFileName,...
     '-I',includeFileName, ...
     '-results-dir',resFolder2,...
     '-misra3','mandatory',...
     '-do-not-generate-results-for','all-headers',...
     '-main-generator');
polyspaceCodeProver('-results-dir',resFolder2);

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

свернуть все

Имя объекта опций Polyspace, заданное как указатель на объект.

Чтобы создать объект опций, используйте один из классов опций Polyspace: polyspace.Options или polyspace.ModelLinkOptions.

Пример: opts

Имя файла проекта с дополнительным .psprj, заданным как вектор символов.

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

Пример: 'C:\Polyspace_Projects\myProject.psprj'

Имя файла результатов с дополнительным .pscp, заданным как вектор символов.

Если файл не находится в текущей папке, resultsFile должен включать полный или относительный путь.

Пример: 'myResults.pscp'

Имя папки результата, заданной как вектор символов. Папка должна содержать файл результатов с дополнительным .pscp. Если файл результатов находится в подпапке заданной папки, эта команда не открывает файл результатов.

Если папка не находится в текущей папке, resultsFolder должен включать полный или относительный путь.

Пример: 'C:\Polyspace\Results\'

Разделенный от запятой исходный файл называет с дополнительным .c или .cpp, заданным как односимвольный вектор.

Если файлы не находятся в текущей папке, sourceFiles должен включать полный или относительный путь.

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

Аргументы в виде пар имя-значение

Укажите необязательные аргументы в виде пар ""имя, значение"", разделенных запятыми. Имя (Name) — это имя аргумента, а значение (Value) — соответствующее значение. Name должен появиться в кавычках. Вы можете задать несколько аргументов в виде пар имен и значений в любом порядке, например: Name1, Value1, ..., NameN, ValueN.

Пример: '-target','i386','-compiler','gnu4.6' указывает, что исходный код предназначается для i386 процессоров и содержит Синтаксис C не-ANSI для компилятора GCC 4.6.

Для полного списка аналитических опций см. Аналитические Опции.

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

|

Введенный в R2013b

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