从编译命令 (makefile) 创建 Polyspace 分析配置

例如，要在持续集成期间定期在服务器上使用脚本运行 Polyspace®，您必须预先配置所有分析选项，以便分析能够无错误地完成。必须根据需要更新这些选项，以跟上新的代码提交。如果您使用编译命令 (makefile) 等现有工件来编译新的代码提交，您可以重复使用编译命令来配置 Polyspace 分析并随时更新新提交。使用 polyspace-configure 命令，您可以监控编译命令的执行，并创建用于 Polyspace 分析的选项文件。

本主题展示了一个简单教程，说明如何从编译命令创建选项文件并将该文件用于后续分析。本主题使用 Linux® makefile 和 GCC 编译器，但您可以调整命令以适应其他操作系统，例如 Windows® 和诸如 Microsoft® Visual Studio® 之类的编译器。

  1. 将演示源文件从 polyspaceserverroot\polyspace\examples\cxx\Bug_Finder_Example\sources 复制到具有写入权限的文件夹。其中，polyspaceserverroot 是 Polyspace 服务器端产品的根安装文件夹，例如 C:\Program Files\Polyspace Server\R2019a。

  2. 创建简单的 makefile 来编译演示源文件。将 makefile 保存在与源文件相同的文件夹中。

    例如，创建一个名为 makefile 的文件并添加以下内容：

    CC := gcc
SOURCES := $(wildcard *.c)

all: $(CC) -c $(SOURCES)
    检查 makefile 是否成功编译了源文件。打开命令行终端，导航到文件夹（使用 cd）并输入：
    make -B
    make 命令应完成执行且无错误。

    -B 选项确保编译 makefile 中的所有目标。通常，make 等编译命令被设置为仅编译自上次编译以来发生更改的源。但是，polyspace-configure 需要完整编译以确定将哪些源添加到 Polyspace 工程或选项文件。

  3. 使用 polyspace-configure 跟踪编译命令并创建一个选项文件 compile_opts。

    polyspace-configure -output-options-file compile_opts make -B

  4. 使用附加选项创建第二个选项文件。例如，创建一个包含以下内容的 run_opts 文件：

    -checkers numerical
-report-template BugFinder
-output-format pdf

    这些选项在 Bug Finder 中运行所有数值检查项，并在分析后使用 BugFinder 模板创建 PDF 报告。

  5. 使用以下两个选项文件运行 Bug Finder 分析：从编译命令创建的 compile_opts 和手动创建的 run_opts。

    Polyspace Bug Finder™:

    polyspace-bug-finder -options-file compile_opts -options-file run_opts

    Polyspace Bug Finder Server™:

    polyspace-bug-finder-server -options-file compile_opts -options-file run_opts

    分析应完成且无错误。您可以在 Polyspace 用户界面中打开结果或将结果上传到 Polyspace Access Web 界面（使用 polyspace-access -upload (Polyspace Access) 命令）。

    要运行 Code Prover 而不是 Bug Finder，请使用 polyspace-code-prover-server 命令而不是 polyspace-bug-finder-server 命令。

您可以使用 MATLAB 脚本运行类似的分析。将 polyspace-bug-finder 替换为 polyspaceBugFinder 函数，将 polyspace-configure 替换为 polyspaceConfigure 函数。

另请参阅

|

另请参阅

主题