为使用 MATLAB Coder 生成的代码配置高级 Polyspace 选项
在使用 Polyspace® 分析生成的代码之前,您可以更改一些默认选项。本主题介绍如何对使用 MATLAB® Coder 生成的代码配置 Polyspace 分析,并重用该配置。
在 R2025a 中: Polyspace 与新的 MATLAB Coder™ App 不兼容。请使用 MATLAB 脚本配置您的 Polyspace 分析。请参阅对从 MATLAB 代码生成的 C/C++ 代码运行 Polyspace
配置 Polyspace 选项
默认的 Polyspace 分析根据默认工程配置运行 Polyspace Code Prover™ 分析。结果存储在当前工作目录下一个名为 result_ 的文件夹中。在分析生成的代码时,您可以使用 project_namepslinkoptions 对象更改这些选项:
opts = pslinkoptions('ec');opts 对象的属性来配置分析。例如:
在 Bug Finder 和 Code Prover 之间进行选择:
% Run Code Prover opts.VerificationMode = 'CodeProver'; % Run Bug Finder opts.VerificationMode = 'BugFinder';
运行 Bug Finder 时,除了检查工程 (
.psprj) 文件中配置的检查项外,还要检查是否违反了 MISRA C:2012 编码规则。opts.VerificationSettings = 'PrjConfigAndMisraC2012';选择输出文件夹名称和位置:
要将每次运行结果保存到新文件夹中,请通过添加后缀使输出文件夹名称唯一:opts.ResultDir = '\results_v1'opts.AddSuffixToResultDir = true;
选择在 MATLAB Coder 使用可能会导致 Code Prover 分析不精确的选项时,是否显示警告或错误:
opt.CheckConfigBeforeAnalysis = 'OnWarn';例如,如果代码生成设置使用 memset 将浮点值和双精度值初始化为 0.0 被禁用,则 Code Prover 可能会因为近似值而显示不精确的橙色检查项。请参阅Orange Checks in Polyspace Code Prover。
有关选项的详细信息,请参阅 pslinkoptions。
共享和重用配置
您可以在 Polyspace 工程文件 (psprj) 中配置高级 Polyspace 选项。该工程文件可用于在不同的 Polyspace 分析之间共享 Polyspace 配置。
要在分析生成代码时使用 psprj 文件中的配置,请使用属性 EnablePrjConfigFile 和 PrjConfigFile:
opts.EnablePrjConfigFile = true;
opts.PrjConfigFile = 'C:\Polyspace\config.psprj';pslinkoptions。