从命令行运行 Polyspace 分析

要从 DOS 或 UNIX® 命令行窗口运行分析，请使用 polyspace-bug-finder 或 polyspace-code-prover 命令，后跟要使用的其他选项。另请参阅：

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

直接指定源和分析选项

在 Windows®、Linux® 或 Mac OS X 命令行中，将源和分析选项追加到 polyspace-bug-finder 或 polyspace-code-prover 命令。

例如：

  • 要指定源，请使用 -sources 选项，后跟以逗号分隔的源列表。

    polyspace-bug-finder -sources C:\mySource\myFile1.c,C:\mySource\myFile2.c

    如果当前文件夹包含具有源文件的 sources 子文件夹，则可以省略 -sources 标志。分析会考虑位于 sources 以及 sources 下的所有子文件夹中的文件。

  • 要指定目标处理器，请使用 -target 选项。例如，要为源文件 file.c 指定 m68k 处理器，请使用以下命令：

    polyspace-bug-finder -sources "file.c" -lang c -target m68k

  • 要检查是否存在违反 MISRA C™ 规则的情形，请使用 -misra2 选项。例如，要仅检查源文件 file.c 中必需的 MISRA C 规则，请使用以下命令：

    polyspace-bug-finder -sources "file.c" -misra2 required-rules

  • 要指定结果文件夹，请使用 -results-dir 选项。

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

  • 可以选择使用 -verif-version 选项指定分析 ID。您可以使用此 ID 来引用分析的不同运行。例如，您可以使用此 ID 从分析的特定运行导入注释。此 ID 还被报告为生成的报告的版本。

有关分析选项的完整列表，请参阅：

要获取完整的选项列表，请在命令行中输入以下命令：

polyspace-bug-finder -help

指定文本文件中的源和分析选项

您可以将选项保存在文本文件中，并在每次运行分析时使用该文本文件，而非直接指定选项。

  1. 使用您的选项创建一个名为 listofoptions.txt 的选项文件。例如：

    #These are the options for MyCodeProverProject
-lang c
-prog MyCodeProverProject
-author jsmith
-sources "mymain.c,funAlgebra.c,funGeometry.c"
-target x86_64
-compiler generic
-dos
-misra2 required-rules
-do-not-generate-results-for all-headers
-main-generator
-results-dir C:\Polyspace\MyCodeProverProject
-ver-f-version 1.0

  2. 使用 listofoptions.txt 文件中的选项运行 Polyspace。

    polyspace-code-prover -options-file listofoptions.txt

另请参阅 -options-file。

从编译系统创建选项文件

如果您使用编译命令 (makefile) 来编译源代码，则可以从编译命令中收集源代码和编译器选项。跟踪您的编译命令以生成具有所需 Polyspace 选项的文本文件。

  1. 使用配置工具创建 Polyspace 选项列表。

    polyspace-configure -output-options-file \
        myOptions buildCommand
    其中，buildCommand 是用于编译源代码的命令，例如 make -B。

    另请参阅polyspace-configure。

  2. 使用从编译命令中读取的选项运行 Polyspace。

    polyspace-bug-finder -options-file myOptions \
        -results-dir myResults

    除了从编译命令中收集的选项之外，您可能还要添加更多选项，例如指定缺陷检查项。您可以将这些选项追加到选项文件中，直接在命令行中或通过另一个选项文件（使用另一个 -options-file 标志）添加它们。

  3. 在 Polyspace 用户界面中打开结果。

    polyspace-bug-finder myResults

另请参阅

| | (Polyspace Code Prover)

主题

外部网站