Запустите верификацию Polyspace Code Prover из MATLAB
Для более легких сценариев запустите анализ Polyspace® с помощью polyspace.Project объект.
polyspaceCodeProver открывает Polyspace Code Prover™.
polyspaceCodeProver( открывает файл проекта Polyspace в Polyspace Code Prover.projectFile)
polyspaceCodeProver( запускает верификацию на объекте опций Polyspace в MATLAB®.optsObject)
polyspaceCodeProver( запускает верификацию на файле проекта Polyspace в MATLAB. Если у вас есть несколько модулей или настроек, Polyspace запускает активную настройку и активный модуль. Чтобы видеть, какой модуль и настройка активны, откройте проект в интерфейсе Polyspace и ищите полужирный, выбранный модуль и настройку. Чтобы измениться, какой модуль или настройка активны, прежде, чем закрыть интерфейс Polyspace, выбирают модуль и настройку, которую вы хотите проверить. projectFile,
'-nodesktop')
polyspaceCodeProver( открывается Polyspace приводит файл к Polyspace Code Prover.resultsFile)
polyspaceCodeProver('-results-dir', открывается Polyspace происходит файл от resultsFolder)resultsFolder в Polyspace Code Prover.
polyspaceCodeProver('-help') отображения все опции, которые могут быть предоставлены polyspaceCodeProver команда, чтобы запустить верификацию Polyspace Code Prover.
polyspaceCodeProver('-sources', запускает верификацию Polyspace Code Prover на исходных файлах, заданных в sourceFiles)sourceFiles.
polyspaceCodeProver('-sources', запускает верификацию Polyspace Code Prover на исходных файлах с дополнительными опциями, заданными одним или несколькими sourceFiles,Name,Value)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.
Создайте, опции возражают и добавляют исходный файл и включают папку в свойства.
opts = polyspace.CodeProverOptions;
opts.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
'cxx', 'Code_Prover_Example', 'sources', 'single_file_analysis.c')};
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
'cxx', 'Code_Prover_Example', 'sources')};
opts.ResultsDir = fullfile(pwd,'results');Запустите верификацию и просмотрите результаты.
polyspaceCodeProver(opts);
polyspaceCodeProver('-results-dir',opts.ResultsDir)В этом примере показано, как запустить верификацию Polyspace в MATLAB с помощью опций DOS/UNIX-style.
Запустите анализ и откройте результаты.
sourceFiles = fullfile(polyspaceroot, 'polyspace', 'examples',... 'cxx', 'Code_Prover_Example', 'sources', 'single_file_analysis.c'); includeFolders = fullfile(polyspaceroot, 'polyspace', 'examples',... 'cxx', 'Code_Prover_Example', 'sources'); resultsDir = fullfile(pwd,'results'); polyspaceCodeProver('-sources',sourceFiles, ... '-I',includeFolders, ... '-results-dir',resultsDir,... '-main-generator'); polyspaceCodeProver('-results-dir',resultsDir);
Этот пример показывает два различных способа настроить верификацию в 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.CodeProverOptions | polyspace.ModelLinkCodeProverOptions