本页翻译不是最新的。点击此处可查看最新英文版本。

在桌面端运行 Polyspace Code Prover

Polyspace® Code Prover™ 是一个可靠的静态分析工具，可证明 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和其他运行时错误。Code Prover 分析无需程序执行、代码插桩或测试用例即可生成结果。Code Prover 使用基于形式化方法的语义分析和抽象解释来确定代码中的控制流和数据流。您可以对手写代码、生成代码或这两者的组合使用 Code Prover。在分析结果中，每个运算都进行了着色，以指示它是否存在运行时错误、是否已证明失败、是否不可达或是否未经证明。

您可以从 Polyspace 用户界面或使用脚本对 C/C++ 代码运行 Code Prover。请参阅：

  • 在用户界面中运行 Polyspace

    如果这是您首次使用 Polyspace，您可能希望从 Polyspace 用户界面开始。您可以从工程设置向导、协助配置和摘要分析日志等功能获得帮助。

  • 在 Windows 或 Linux 命令行上运行 Polyspace

    在 Polyspace 用户界面中设置工程并完成几次试运行后，您可以将配置导出为自动或按需运行的脚本。您还可以直接从操作系统中的命令行直接运行 Polyspace 分析。然后，您可以将命令保存在批处理文件 (Windows) 或 shell 脚本 (Linux) 中供以后运行。如果您使用持续集成工具（例如 Jenkins®）运行 Polyspace Server 端产品，则可以从 Polyspace 桌面端产品重复使用您的脚本。

  • 在 MATLAB 中运行 Polyspace

    如果您安装了 MATLAB®，编写脚本来运行 Polyspace 分析则会特别容易。您可以利用在 MATLAB 环境中编写脚本的所有优势，例如，有关函数语法的自动帮助。分析后，您可以使用 MATLAB 图形和可视化工具创建自己的可视化结果。

示例文件

要遵循本教程中的步骤，请从 polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources 中将文件 example.c 和 include.h 复制到另一个文件夹。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2020a。

在用户界面中运行 Polyspace

打开 Polyspace 用户界面

双击 polyspaceroot\polyspace\bin 中的 polyspace 可执行文件。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2020a。另请参阅安装文件夹。

如果您在桌面端或者在 Windows® 的开始菜单中设置了 Polyspace 的快捷方式，请双击该快捷方式。

添加源文件

要运行验证，您必须新建一个新的 Polyspace 工程。Polyspace 工程指向您的文件系统上的源文件夹和包含文件夹。

在起始页窗格的左侧，点击启动新工程。或者，选择文件 > 新建工程。

提供工程名称后，在接下来的屏幕上：

  • 添加您的源文件夹。

    在本教程中，请添加您已在其中保存文件 example.c 的文件夹的路径。点击下一步。

  • 添加您的包含文件夹。

    在本教程中，请添加您已在其中保存文件 include.h 的文件夹的路径。此文件夹可以与前一个文件夹相同。然后，点击完成。

源文件夹和包含文件夹添加完成后，您会在工程浏览器窗格中看到一个新工程。您的源文件夹将被复制到工程中的第一个模块。您可以在以后通过右键点击工程来添加更多文件夹。如果您以后添加文件夹，则必须显式将其复制到一个模块。

配置并运行 Polyspace

您可以更改与 Polyspace 分析关联的默认选项。

点击您的工程模块中的配置节点。在配置窗格上，根据需要更改选项。例如，在编码规则和代码度量节点上，选择检查 MISRA C:2004。

有关详细信息，请查看每个选项的工具提示。点击更多帮助链接可了解有关选项的快捷帮助。

要启动验证，请点击顶部工具栏中的运行 Code Prover。如果该按钮指示的是 Bug Finder，请点击按钮旁边的箭头来切换到 Code Prover。

在输出摘要窗口上关注分析进度。验证完成后，结果将自动打开。

其他信息

请参阅：

在 Windows 或 Linux 命令行上运行 Polyspace

您可以通过 Windows 或 Linux® 命令行使用批处理 (.bat) 文件或 shell (.sh) 脚本运行 Code Prover。

使用 polyspace-code-prover 命令运行验证。

为免于键入命令的完整路径，请将路径 polyspaceroot\polyspace\bin 添加到您的操作系统上的 Path 环境变量。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2024b。

导航到已保存文件的文件夹（使用 cd）。输入以下命令：

polyspace-code-prover -sources example.c -I . -results-dir . -main-generator
其中，. 表示当前文件夹。使用的选项包括：

  • -sources：指定逗号分隔的源文件。

  • -I：指定包含文件夹的路径。每次要添加单独的包含文件夹时，请使用 -I 标志。

  • -results-dir：指定将保存 Polyspace Code Prover 结果的文件夹的路径。

    请注意，每次运行时都会清理并重新填充结果文件夹。为避免在清理过程中意外删除文件，请为 Polyspace 结果指定一个专用文件夹，而不是使用包含其他文件的现有文件夹。

  • 验证模块或库 (-main-generator)：指定如果在源文件中找不到 main 函数，则必须生成该函数

验证完成后，结果将保存在 ps_results.pscp 文件中。您可以从 Polyspace 用户界面打开此文件。例如，输入以下命令：

polyspace ps_results.pscp

除了直接在命令行上指定逗号分隔的源文件之外，您还可以将源文件列在一个文本文件中（每行一个文件）。可以使用 -sources-list-file 选项指定此文本文件。

其他信息

请参阅：

在 MATLAB 中运行 Polyspace

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

要运行分析，请使用 polyspace.Project 对象。该对象有两个属性：

  • Configuration:可以使用此属性指定分析选项，例如源文件夹、包含文件夹、编译器文件夹和结果文件夹。

  • Results:分析完成后，可以使用此属性将分析结果读取到一个 MATLAB 表中。

要运行分析，请使用此对象的 run 方法。

要对 polyspaceroot\polyspace\examples\cxx\Code_Prover_Examples\sources 中的示例文件 example.c 运行 Polyspace，请在 MATLAB 命令提示符处输入以下命令。

proj = polyspace.Project

% Configure analysis
proj.Configuration.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources', 'example.c')};
proj.Configuration.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot,...
 'polyspace', 'examples', 'cxx', 'Code_Prover_Example', 'sources')};
proj.Configuration.TargetCompiler.Compiler = 'gnu4.9';
proj.Configuration.ResultsDir = fullfile(pwd,'results');
proj.Configuration.CodeProverVerification.MainGenerator = true;


% Run analysis
cpStatus = proj.run('codeProver');

% Read results
resObj = proj.Results;
cpSummary = getSummary(resObj, 'runtime');
cpResults = getResults(resObj, 'readable');

验证完成后，结果将保存在 ps_results.pscp 文件中。您可以从 Polyspace 用户界面打开此文件。例如，输入以下命令：

resultsFile = fullfile(proj.Configuration.ResultsDir,'ps_results.pscp');
polyspaceCodeProver(resultsFile)

其他信息

请参阅：

另请参阅

主题