Запуск проверки средства проверки кода Polyspace из MATLAB
Для упрощения создания сценариев запустите анализ Polyspace ® с помощью polyspace.Project объект.
polyspaceCodeProver открывает Prover™ Polyspace Code.
status = polyspaceCodeProver(projectFile)
status = polyspaceCodeProver(optsObject)
status = polyspaceCodeProver(projectFile, '-nodesktop')
status = polyspaceCodeProver(resultsFile)
status = polyspaceCodeProver('-results-dir',resultsFolder)resultsFolder в программе Polyspace Code Prover.
status = polyspaceCodeProver('-help')polyspaceCodeProver для выполнения проверки средства проверки кода Polyspace.
status = polyspaceCodeProver('-sources',sourceFiles)sourceFiles.
polyspaceCodeProver('-sources', выполняет проверку Polyspace Code Prover для исходных файлов с дополнительными параметрами, указанными одним или несколькими sourceFiles,Name,Value)Name,Value аргументы пары.
Примечание
Перед запуском Polyspace из MATLAB необходимо связать установки Polyspace и MATLAB. См. раздел Интеграция полиспейса с 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 с использованием объектов.
Создайте объект options, добавьте исходный файл и включите папку в свойства.
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.
Выполните анализ и откройте результаты.
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. Можно настроить любое количество дополнительных опций, изменив свойства объекта опций или используя пары Наименование (Name) - Значение (Value). Необходимо указать проверку правил кодирования 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');
Проверьте правила кодирования с помощью объекта options.
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);