Запустите верификацию Polyspace Code Prover из MATLAB
Для более легкого скриптирования запустите Polyspace® анализ с использованием polyspace.Project объект.
polyspaceCodeProver Открывает Polyspace Code Prover™.
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 Code Prover.
status = polyspaceCodeProver('-sources',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 _ результат
Присвойте полный путь к папке переменного 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.
Запустите анализ и откройте результаты.
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. Можно настроить любое количество дополнительных опций путем изменения свойств в объекте options или с помощью пар "имя-значение". Вы задаете проверку 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);