对从 MATLAB 代码生成的 C/C++ 代码运行 Polyspace

R2026b

此示例使用:

从 MATLAB® 代码生成 C/C++ 代码后，您可以独立地检查生成代码中的问题：

  • 使用 Polyspace® Bug Finder™ 检查错误或缺陷以及编码违规。

  • 使用 Polyspace Code Prover™ 检查运行时错误。

在 R2025a 中: Polyspace 与新的 MATLAB Coder™ App 不兼容。请使用 MATLAB 脚本进行 Polyspace 分析，具体操作请参阅本主题。

前提条件

要运行此示例：

  • 您必须拥有 Embedded Coder® 许可证。

  • 您应该已经熟悉如何使用 codegen 命令。否则，请参阅 MATLAB Coder 快速入门。

  • 您必须将 Polyspace 与 MATLAB 安装进行集成。请参阅将 Polyspace 与 MATLAB 和 Simulink 集成。

示例文件

本教程使用 polyspaceroot\polyspace\examples\doc_cxx\matlab_coder 中的 MATLAB Coder 示例 averaging_filter。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2026b。此示例显示了 Code Prover 的分析。对于 Bug Finder，您可以遵循类似的工作流。

使用 MATLAB 运行 Polyspace 分析

要运行 Polyspace 分析，首先需要将 MATLAB 函数 averaging_filter() 生成的 C 代码作为静态库。在 MATLAB 命令窗口中，输入：

% Generate code
matlabFileName = fullfile(polyspaceroot, 'polyspace',...
    'examples','doc_cxx','matlab_coder','averaging_filter.m');
codegenFolder = fullfile(pwd, 'codegenFolder');
codegen(matlabFileName, '-config:lib', '-c', '-args', ...
   {zeros(1,100,'double')}, '-d', codegenFolder);

您可以通过以下两种方式之一运行 Polyspace 分析：

  • 使用 polyspace.ModelLinkOptions - 此类提供对所有 Polyspace 选项的访问权限，并可用于运行自定义分析。

  • 使用 pslinkrun - 通过此函数可在不使用任何类的情况下快速编写分析脚本。

使用 polyspace.Project 运行完全配置的分析

将 polyspace.ModelLinkOptions 对象与生成的代码关联。-codegenfolder 选项会自动从代码生成输出中发现源文件、包含路径和编译器设置。

psprjCfg = polyspace.ModelLinkOptions('-codegenfolder', codegenFolder);

使用 polyspace.ModelLinkOptions 对象，您可以详细配置 Polyspace Code Prover 验证。例如，使用属性 psprjCfg.Precision 调节验证精度。精度级别越高，所需完成时间越长，所产生结果的精确度越高。

psprjCfg.Precision.OLevel = 2;
psprjCfg.Precision.To = 'Software Safety Analysis level 2';

配置分析，以使用 Developer 模板生成 PDF 报告。

psprjCfg.MergedReporting.EnableReportGeneration = true;
psprjCfg.MergedReporting.CodeProverReportTemplate = 'Developer';
psprjCfg.MergedReporting.ReportOutputFormat = 'PDF';

指定用于存放分析结果的文件夹。

psprjCfg.ResultsDir = fullfile(pwd, 'codeprover_results');

创建一个 polyspace.Project 对象。将此对象的 Configuration 属性与您之前指定的选项关联。运行分析并打开结果。

proj = polyspace.Project;
proj.Configuration = psprjCfg;
cpStatus = proj.run('codeProver');
proj.Results.getResults('readable');

使用 pslinkrun 运行快速分析

创建一个 pslinkoptions 对象来配置 Polyspace 分析。在 MATLAB 命令窗口中，输入：

opts = pslinkoptions('ec');
通过设置 opts 对象的属性，可以选择 Code Prover 的一种验证模式，将结果存储在临时文件夹中，并在分析完成后打开 Polyspace 用户界面：
opts.VerificationMode = 'CodeProver';
opts.ResultDir = [tempdir 'results'];
opts.OpenProjectManager = 1;

使用上述配置运行 Polyspace 分析：

[polyspaceFolder, resultsFolder] = pslinkrun('-codegenfolder', codegenFolder, opts);
如果分析完成且无错误，则 Polyspace 结果会自动打开。

另请参阅

|

主题