polyspaceCodeProverServer

从 MATLAB 运行 Polyspace Code Prover 验证

全页折叠

为了更轻松地编写脚本，请使用 polyspace.Project 对象运行 Polyspace® 分析。

语法

polyspaceCodeProverServer(optsObject)
polyspaceCodeProverServer('-help')
polyspaceCodeProverServer('-sources',sourceFiles)
polyspaceCodeProverServer('-sources',sourceFiles,Name,Value)

说明

polyspaceCodeProverServer(optsObject) 对 MATLAB® 中的 Polyspace 选项对象运行验证。

示例

polyspaceCodeProverServer('-help') 显示可以提供给 polyspaceCodeProverServer 命令以运行 Polyspace Code Prover™ 验证的所有选项。

polyspaceCodeProverServer('-sources',sourceFiles) 对在 sourceFiles 中指定的源文件运行 Polyspace Code Prover 验证。

示例

polyspaceCodeProverServer('-sources',sourceFiles,Name,Value) 使用一个或多个 Name,Value 对组参量指定的附加选项对源文件运行 Polyspace Code Prover 验证。

注意

在从 MATLAB 中运行 Polyspace 之前，必须将已安装的 Polyspace 与 MATLAB 相关联。请参阅将 Polyspace Server 产品与 MATLAB 集成。

示例

示例

全部折叠

此示例显示了如何从 MATLAB 命令行运行 Polyspace 验证。对于此示例：

  • 使用位于目录 polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources 中的源文件 numerical.c。

  • 包括位于同一目录中的头文件。

创建一个选项对象并将源文件和包含文件夹添加到属性中。

opts = polyspace.Options;
opts.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c')};;
opts.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources')};
opts.ResultsDir = 'C:\Polyspace_Results';

运行分析并查看结果。

polyspaceCodeProverServer(opts);

Code Prover 分析针对文件 C:\Polyspace_Sources\source.c 运行，并将结果存储在 C:\Polyspace_Results 中。

此示例显示了如何使用 DOS/UNIX 选项对单个源文件运行 Polyspace 验证。对于此示例：

  • 使用位于目录 polyspaceroot/polyspace/examples/cxx/BugFinder_example/sources 中的源文件 numerical.c。

  • 包括位于同一目录中的头文件。

定义源文件和包含文件的位置。

src = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources', 'numerical.c');
inc = fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Bug_Finder_Example', 'sources');
res = fullfile(pwd,'results');

运行验证并打开结果。

polyspaceCodeProverServer('-sources',src, ...
    '-I',inc, ...
    '-results-dir',res)

此示例显示了在 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.EnableMisraC3 = true;
opts.CodingRulesCodeMetrics.MisraC3Subset = 'mandatory';
opts.CodeProverVerification.EnableMain = true;
opts.InputsStubbing.DoNotGenerateResultsFor = 'all-headers';
polyspaceCodeProverServer(opts);

使用 DOS/UNIX 选项验证编码规则。

polyspaceCodeProverServer('-sources',sourceFileName,...
     '-I',includeFileName, ...
     '-results-dir',resFolder2,...
     '-misra3','mandatory',...
     '-do-not-generate-results-for','all-headers',...
     '-main-generator');

输入参数

全部折叠

Polyspace 选项对象名称，指定为对象句柄。

要创建选项对象，请使用以下 Polyspace 选项类之一：polyspace.Options 或 polyspace.Project。

示例: opts

以逗号分隔的、扩展名为 .c 或 .cpp 的源文件名称，指定为单个字符向量。

如果文件不在当前文件夹中，则 sourceFiles 必须包含完整路径或相对路径。

示例: 'myFile.c', 'C:\mySources\myFile1.c,C:\mySources\myFile2.c'

名称-值参数

将可选参量对组指定为 Name1=Value1,...,NameN=ValueN，其中 Name 是参量名称，Value 是对应的值。名称-值参量必须出现在其他参量之后，但对各个参量对组的顺序没有要求。

在 R2021a 之前，使用逗号分隔每个名称和值，并将 Name 用引号引起来。

示例: '-target','i386','-compiler','gnu4.6' 指定该源代码用于 i386 处理器，并包含 GCC 4.6 编译器的非 ANSI C 语法。

有关分析选项的完整列表，请参阅Polyspace Code Prover 分析选项的完整列表。

版本历史记录

在 R2019a 中推出

另请参阅

主题