polyspaceCodeProver
从 MATLAB 运行 Polyspace Code Prover 验证
为了更轻松地编写脚本，请使用 polyspace.Project 对象运行 Polyspace® 分析。
语法
说明
polyspaceCodeProver 打开 Polyspace Code Prover™。
status = polyspaceCodeProver(projectFile)
status = polyspaceCodeProver(optsObject)
注意
使用 Polyspace 选项对象运行分析时，仅使用 Polyspace 选项对象指定分析选项。第一个参量是 Polyspace 选项对象时，不支持使用名称-值参量。
status = polyspaceCodeProver(projectFile, '-nodesktop')
status = polyspaceCodeProver(resultsFile)
status = polyspaceCodeProver('-results-dir',resultsFolder)resultsFolder 打开一个 Polyspace 结果文件。
status = polyspaceCodeProver('-help')polyspaceCodeProver 命令来运行 Polyspace Code Prover 验证的所有选项。
status = polyspaceCodeProver('-sources',sourceFiles)sourceFiles 中指定的源文件运行 Polyspace Code Prover 验证。
polyspaceCodeProver('-sources', 使用一个或多个 sourceFiles,Name,Value)Name,Value 对组参量指定的附加选项对源文件运行 Polyspace Code Prover 验证。
注意
在从 MATLAB 中运行 Polyspace 之前，必须将已安装的 Polyspace 与 MATLAB 相关联。请参阅将 Polyspace 与 MATLAB 和 Simulink 集成。
[ 将分析负载转移到远程集群。其中，status, jobID] = polyspaceCodeProver(___,'-batch','-scheduler',scheduler)scheduler 指定集群的主节点，该节点管理来自多个客户端的分析提交。另请参阅操作集群中的两个作业。
示例
从 MATLAB 打开 Polyspace 工程
此示例显示了如何从 MATLAB 打开具有扩展名 .psprj 的 Polyspace 工程文件。在此示例中，打开工程文件 Code_Prover_Example.psprj。
将完整的工程文件路径指定给 MATLAB 变量 prjFile。
prjFile = fullfile(polyspaceroot, 'polyspace', 'examples', 'cxx', ... 'Code_Prover_Example', 'Code_Prover_Example.psprj');
打开该工程。
polyspaceCodeProver(prjFile)
从 MATLAB 打开 Polyspace 结果
此示例显示了如何从 MATLAB 打开一个 Polyspace 结果文件。在此示例中，您从文件夹 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 中运行 Polyspace 验证。
创建一个选项对象并将源文件和包含文件夹添加到属性中。
opts = polyspace.Options;
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)使用 DOS/UNIX 选项从 MATLAB 运行 Polyspace 验证
此示例显示了如何使用 DOS/UNIX 样式的选项在 MATLAB 中运行 Polyspace 验证。
运行分析并打开结果。
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);
运行带编码规则检查的 Polyspace 验证
此示例显示了在 MATLAB 中自定义验证的两种不同方法。您可以通过更改选项对象中的属性或使用名称-值对组，自定义任意数量的附加选项。您可以指定检查 MISRA C™ 2012 编码规则，从编码规则检查中排除头文件，并生成 main。
为源文件路径、包含文件夹路径和结果文件夹路径创建变量，以便可以将其用于任一分析方法。
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.Options('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);
输入参数
名称-值参数
输出参量
版本历史记录
在 R2013b 中推出
