本页采用了机器翻译。点击此处可查看最新英文版本。

polyspace-configure

（系统命令）从 DOS 或 UNIX 命令行中的编译系统创建 Polyspace 工程

全页折叠

语法

polyspace-configure buildCommand
polyspace-configure [options] buildCommand
polyspace-configure [options] -compilation-database jsonFile

说明

polyspace-configure 系统命令从编译命令创建一个 Polyspace® 工程或选项文件。

注意

此 Polyspace 命令在 polyspaceroot\polyspace\bin 中可用。这里，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2025a（请参阅适用于桌面端产品的安装文件夹或适用于服务器产品的安装文件夹）。为避免键入此命令的完整路径，请将此位置添加到操作系统中的 PATH 环境变量中。

polyspace-configure buildCommand 跟踪您的编译系统，并使用从编译系统收集的信息创建一个 Polyspace 工程。只有当您的编译命令或 makefile 满足某些要求时，Polyspace 才会从您的编译系统创建一个工程。有关编译器和编译命令的要求（包括 Polyspace 支持的编译器列表），请参阅 从编译系统创建工程的要求。

示例

polyspace-configure [options] buildCommand 跟踪您的编译系统，并使用 options 修改 polyspace-configure 的默认操作。在 buildCommand 之前指定修饰符，否则它们将被视为编译命令本身的选项。

示例

polyspace-configure [options] -compilation-database jsonFile 使用您提供的 JSON 编译数据库文件 jsonFile 中收集的信息创建一个 Polyspace 工程。您无需指定编译命令或跟踪编译系统。有关 JSON 编译数据库的更多信息，请参阅 JSON 编译数据库。

示例

示例

全部折叠

此示例展示了如何使用编译命令创建 Polyspace 工程。运行 polyspace-configure 的最简单方法是在用于编译源代码的编译命令上直接运行它。此示例使用 GCC 编译器和编译命令 gcc。GCC 是一套标准编译器工具集，随 Linux® 基于的系统一同提供。对于基于 Windows® 的系统，可以安装 MinGW 以支持 GCC 编译器。

首先，确保您的源代码能够编译且无错误。 

gcc myFilename.c otherFile.c
在确认源代码编译无误后，请删除对象文件，然后继续。
rm myFilename.o otherFile.o

创建一个名为 Polyspace 的工程，并指定一个唯一的工程名称。在编译命令中运行 polyspace-configure，与之前测试时相同。

polyspace-configure -prog myProject gcc myFilename.c otherFile.c

在 Polyspace 用户界面中打开 Polyspace 工程。

如果您使用 Visual Studio® 编译源代码，则可以将上述示例中的 gcc 替换为 cl。您还可以在 Visual Studio 工程的完整编译上运行 polyspace-configure。请参阅Create Polyspace Projects from Visual Studio Build。

请注意，polyspace-configure 使用编译命令中的源代码创建了一个新的 Polyspace 工程。无法使用 polyspace-configure 命令将内容附加到已存在的 Polyspace 工程中。如果您使用编译选项（例如 -D 代表 gcc），则 polyspace-configure 会在工程中设置等效的 Polyspace 选项。有关更多详细信息，请参阅算法。

此示例展示了如何使用编译命令创建一个 Polyspace Platform (Polyspace Test) 工程。运行 polyspace-configure 的最简单方法是在用于编译源代码的编译命令上直接运行它。此示例使用 GCC 编译器和编译命令 gcc。GCC 是一套标准编译器工具集，随 Linux 基于的系统一同提供。对于基于 Windows 的系统，可以安装 MinGW 以支持 GCC 编译器。

首先，确保您的源代码能够编译且无错误。 

gcc myFilename.c otherFile.c
在确认源代码编译无误后，请删除对象文件，然后继续。
rm myFilename.o otherFile.o

创建一个指定唯一工程名称的 Polyspace 平台工程。在编译命令中运行 polyspace-configure，与之前测试时相同。

polyspace-configure -output-platform-project myProject gcc myFilename.c otherFile.c

在 Polyspace 平台用户界面中打开 Polyspace 工程。

如果您使用 Visual Studio 编译源代码，则可以将上述示例中的 gcc 替换为 cl。您还可以在 Visual Studio 工程的完整编译上运行 polyspace-configure。请参阅Create Projects from Visual Studio in Polyspace Platform User Interface (Polyspace Test)。

通常，在实际应用中，您不会直接调用编译器来编译源代码。您的编译命令会运行多个命令，其中之一是编译。例如，您可能正在运行一个 makefile 来编译源代码。此示例演示了如何使用命令 make targetName buildOptions 编译源代码来创建 Polyspace 工程。

创建一个名为 Polyspace 的工程，并指定一个唯一的工程名称。将 -B 或 -W makefileName 选项与 make 一起使用，以便重新制作 makefile 中的所有前提条件目标。

polyspace-configure  -prog myProject \
make -B targetName buildOptions

在 Polyspace 用户界面中打开 Polyspace 工程。

此示例展示了如何从使用 CMake 编译系统生成器生成的 JSON 编译数据库创建 Polyspace 选项文件。CMake 为指定的编译工具生成编译指令，例如 UNIX® 的 make Makefiles 或 Microsoft® Visual Studio 的工程文件。CMake 仅支持为 Makefile 生成器和 Ninja 生成器生成 JSON 编译数据库。有关更多信息，请参阅 makefile 生成器。

为您的 CMake 工程生成一个 JSON 编译数据库。Cmake 工程示例，请参阅 polyspaceroot\polyspace\examples\doc_cxx\compilation_database，其中 polyspaceroot 是您的 Polyspace 安装文件夹。

导航到工程源代码树的根目录。该文件夹包含 CMake 用于生成编译指令的输入文件 CMakeLists.txt。输入以下命令：

mkdir JSON_cdb
cd JSON_cdb
cmake -G "Unix Makefiles" -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../
最后一条命令生成一个名为 UNIX 的 makefile，其中包含用于 make 编译工具的编译说明。该命令还会输出文件 compile_commands.json。此文件列出了工程中每个翻译单元的编译器调用。

从上一步生成的编译数据库中生成一个 Polyspace 选项文件。

polyspace-configure -compilation-database compile_commands.json \
-output-options-file options.txt
您无需指定编译命令，polyspace-configure 不会跟踪您的编译。Polyspace 从 JSON 编译数据库中提取有关您的编译系统的信息。

将选项文件传递给 Polyspace 以运行分析，例如：

polyspace-bug-finder -options-file options.txt

此示例展示了如何从编译系统的同一跟踪创建不同的 Polyspace 工程。您可以指定每个工程要包括的源文件。

通过指定选项 -no-project，无需创建 Polyspace 工程即可跟踪编译系统。为了确保 makefile 中所有前提条件目标都重新编译，请使用相应的 make 编译命令选项，例如 -B。

polyspace-configure -no-project make -B

polyspace-configure 将缓存信息和编译跟踪信息存储在当前文件夹内的默认位置。要将缓存信息存储在其他位置并编译跟踪，请指定选项 -cache-path 和 -build-trace。

使用上一步的编译跟踪信息生成 Polyspace 工程。指定工程名称，并使用 -include-sources 或 -exclude-sources 选项选择要包含在每个工程中的文件。

polyspace-configure -no-build -prog myProject \
-include-sources "glob_pattern"

glob_pattern 是一个全局模式，对应于您在工程中过滤或排除的文件夹或文件。要确保 shell 不会展开您传递到 polyspace-configure 的 glob 模式，请将它们括在双引号中。有关全局模式支持的语法详细信息，请参阅 使用模式匹配选择用于 Polyspace 分析的文件。

如果您在上一步中指定了选项 -build-trace 和 -cache-path，请再次指定它们。

删除跟踪文件和缓存文件夹。

rm -r polyspace_configure_cache polyspace_configure_build_trace
如果您使用了选项 -build-trace 和 -cache-path，请使用这些选项中的路径和文件名。

此示例显示了如何使用命令 make targetName buildOptions 编译源代码后运行 Polyspace 分析。在此示例中，您使用 polyspace-configure 来跟踪编译系统，但未创建 Polyspace 工程。相反，您可以创建一个选项文件，用于从命令行运行 Polyspace 分析。

创建一个指定 -output-options-file 命令的 Polyspace 选项文件。将 -B 或 -W makefileName 选项与 make 一起使用，以便重新制作 makefile 中的所有前提条件目标。

polyspace-configure -output-options-file\
 myOptions make -B targetName buildOptions

使用您创建的选项文件在命令行中运行 Polyspace 分析：

polyspace-bug-finder -options-file myOptions

输入参数

全部折叠

编译命令与您编译源代码时使用的完全一致。

编译命令必须对源代码进行完整编译，而不是增量编译。通常，make 等编译命令被设置为仅编译自上次编译以来发生更改的源。但是，polyspace-configure 需要完整编译以确定将哪些源添加到 Polyspace 工程或选项文件。在编译命令中添加适当的选项，强制进行完整编译。例如，使用 makefile 时，将选项 -B 附加到 make。

示例: make -B, make -B -W makefileName

选项描述
-prog projectName

在 Polyspace 用户界面中显示的工程名称。默认值为 polyspace。

如果不使用选项 -output-project，则 -prog 参量也会设置工程名称。

示例： -prog myProject 在用户界面中创建了一个名为 myProject 的工程。如果您不使用选项 -output-project，工程名称也将为 myProject.psrprj。

-author authorName

工程作者姓名。

示例：-author jsmith

-output-project filePath

Polyspace 工程文件的路径。默认文件为当前文件夹中的 polyspace.psprj 文件。

示例： -output-project ../myProjects/project1 在相对路径为 ../myProjects/ 的文件夹中创建了一个名为 project1.psprj 的工程。

-output-platform-project filePath

Polyspace 平台工程文件或工作区文件的路径（如果您使用的是选项 -module、-modules-list 或 -module-output-pattern）。Polyspace 将文件保存到当前文件夹中。

示例：-output-platform-project ../myProjects/project1 在相对路径为 ../myProjects/ 的文件夹中创建一个名为 project1.psprjx 的工程。

示例：-output-platform-project ../myProjects/workspace1 -module 在相对路径为 ../myProjects/ 的文件夹中创建工作区文件 project1.pswkps。

有关 Polyspace 平台工程的更多信息，请参阅：

-update-platform-project filePath

使用此选项，可使用当前工程运行的配置更新 Polyspace 平台工程 (.psprjx) 的编译配置。filePath 参量可以是相对的或绝对的。如果处理器配置已存在，则该命令将使用该配置作为新编译配置。

如果指定的工程不存在，则该命令将创建一个新工程。

示例：polyspace-configure -update-platform-project ../myProjects/myProject.psprjx

-output-options-file filePath

Polyspace 生成的分析选项文件的路径。使用此文件进行命令行分析，可使用以下命令之一：

  • polyspace-bug-finder

  • polyspace-code-prover

  • polyspace-bug-finder-server

  • polyspace-code-prover-server

  • polyspace-bug-finder-access

-allow-build-error

即使在编译过程中出现错误，也创建 Polyspace 工程的选项。

如果发生错误，编译跟踪日志将显示以下消息：

polyspace-configure (polyspaceConfigure) 
   ERROR: build command 
   command_name fail [status=status_value]
command_name 是您使用的编译命令名称，status_value 是非零退出状态或错误级别，用于指示编译过程中发生的错误。

如果编译命令编译了源文件但以非零退出状态退出，则此选项可创建一个有用的工程。如果源文件无法编译且编译失败，请在再次使用 polyspace-configure 之前解决编译失败的问题。

当使用 -compilation-database 时，此选项将被忽略。

-allow-overwrite

如果存在同名工程，则覆盖该工程。

默认情况下，如果输出文件夹中已存在同名的工程，polyspace-configure (polyspaceConfigure) 会抛出错误。使用此选项可覆盖工程。

-no-console-output

-silent（默认）

-verbose

抑制或显示运行 polyspace-configure (polyspaceConfigure) 时出现的附加消息的选项。

  • -no-console-output - 抑制所有输出，包括错误和警告。

  • -silent（默认）- 仅显示错误和警告。

  • -verbose - 显示所有消息。

如果指定了多个选项，则应用最详细的选项。

当您将这些选项与 -easy-debug 组合使用时，Polyspace 会忽略这些选项。

-help

显示 polyspace-configure (polyspaceConfigure) 命令的完整列表的选项

-debug

存储调试信息供 MathWorks® 技术支持使用的选项。

此选项已被选项 -easy-debug 取代。

-easy-debug folderPath

Polyspace 存储供 MathWorks 技术支持使用的调试信息的文件夹路径。

在执行一次 polyspace-configure (polyspaceConfigure) 操作后，文件夹 folderPath 中会包含一个以 pscfg-output.zip 结尾的压缩文件。如果运行无法创建完整的 Polyspace 工程或选项文件，请将此压缩文件发送至 MathWorks 技术支持，以进行进一步调试。压缩文件中不包含编译过程中追踪到的源文件。另请参阅Errors in Project Creation from Build Systems。

选项描述
-module

为在编译系统中创建的每个二进制文件创建单独的分析模块的选项。

构成分析模块的内容取决于 polyspace-configure 命令的输出：

  • 如果将选项 -module 与选项 -output-project projectName 一起使用，则该命令将生成一个名为 projectName.psprj 的文件，其中每个二进制文件对应一个模块。

  • 如果将选项 -module 与选项 -output-options-path pathName 一起使用，则该命令将在文件夹 pathName 中为每个二进制文件生成一个选项文件。

  • 如果将选项 -module 与选项 -output-platform-project workspaceName 一起使用，则 Polyspace 会创建一个工作区文件 (workspaceName.pswks)，其中包含一个二进制文件对应的一个 Polyspace 平台工程 (.psprjx)。有关工作区的更多信息，请参阅 Manage Related Projects in Polyspace Platform User Interface Using Workspaces。

此选项仅在以下情况下受支持：

  • 如果您使用以下链接器中的一个从编译命令创建工程或选项文件：

    • GNU® - ld、gold 或 ar 链接器。

    • Visual C++® - link.exe 链接器。

  • 如果您从 CMake JSON 编译数据库创建工程或选项文件。

请注意，当您以这种方式为每个二进制文件创建单独的选项文件时，每个选项文件都包含直接参与二进制文件的源文件，而不通过共享对象。有关详细信息，请参阅Modularize Polyspace Analysis by Using Build Command。

-modules-list fileWithModuleList

为文本文件 fileWithModuleList 中指定的每个根文件夹创建单独输出的选项。在文本文件中，每行指定一个根文件夹。对于该文本文件中列出的每个根文件夹，polyspace-configure 命令会创建仅由该根文件夹中的源文件组成的单独分析模块。除非使用选项 -project-root，否则根文件夹路径将根据当前工作文件夹进行解析。

构成分析模块的内容取决于 polyspace-configure 命令的输出：

  • 如果将选项 -modules-list 与选项 -output-options-path pathName 一起使用，则该命令将在文件夹 pathName 中为每个根文件夹生成一个选项文件。

  • 如果将选项 -modules-list 与选项 -output-platform-project workspaceName 一起使用，则 Polyspace 会创建一个工作区文件 (workspaceName.pswks)，其中每个根文件夹包含一个 Polyspace Platform 工程 (.psprjx)。有关工作区的更多信息，请参阅 Manage Related Projects in Polyspace Platform User Interface Using Workspaces。

无论您是从编译命令还是 JSON 编译数据库创建工程或选项文件，此选项都受支持。

-module-output-pattern regex

为正则表达式 regex 捕获的每个根文件夹创建单独输出的选项。在正则表达式中指定一个捕获组。对于正则表达式捕获的每个根文件夹，polyspace-configure 命令会创建一个独立的分析模块，该模块仅包含该根文件夹中的源文件。根文件夹路径已解析：

  • 对于运行编译命令的文件夹，如果您从编译命令创建分析模块，则会创建一个名为 "compiled" 的文件夹。

  • 关于您在 JSON 编译数据库中的 directory 条目，如果您从 JSON 编译数据库创建分析模块。

构成分析模块的内容取决于 polyspace-configure 命令的输出：

  • 如果将选项 -module-output-pattern 与选项 -output-options-path pathName 一起使用，则该命令将在文件夹 pathName 中为每个根文件夹生成一个选项文件。

  • 如果将选项 -module-output-pattern 与选项 -output-platform-project workspaceName 一起使用，则 Polyspace 会创建一个工作区文件 (workspaceName.pswks)，其中每个根文件夹包含一个 Polyspace Platform 工程 (.psprjx)。有关工作区的更多信息，请参阅 Manage Related Projects in Polyspace Platform User Interface Using Workspaces。

无论您是从编译命令还是 JSON 编译数据库创建工程或选项文件，此选项都受支持。

-output-options-path folderPath

生成选项文件的保存路径。将此选项与选项 -module 或 -modules-list 一起使用。

选项文件以在编译系统中创建的二进制文件命名。

-project-root folderPath解析根文件夹路径的文件夹路径。将此选项与选项 -modules-list 一起使用。如果省略此选项，则根据当前工作文件夹解析 -modules-list 提供的文本文件中的根文件夹路径。
选项描述
-compilation-database filePath

JSON 编译数据库 (JSON CDB) 文件的路径。您可以从编译系统生成此文件，例如使用标记 -DCMAKE_EXPORT_COMPILE_COMMANDS=1 与 cmake。该文件包含工程中所有翻译单元的编译器调用。有关详细信息，请参阅 JSON 编译数据库。polyspace-configure 使用此文件的内容来获取有关您的编译系统的信息。从 JSON CDB 中提取的编译器路径必须可从运行 polyspace-configure 的路径访问。

使用此选项时，无需指定编译命令。

这些编译系统和编译器支持生成 JSON CDB：

  • CMake

  • Bazel

  • Clang

  • Ninja

  • Qbs

  • waf

此选项与 -no-project 以及创建多个模块的选项不兼容。

使用此选项时，Polyspace 会忽略缓存控制选项 -allow-build-error 和 -no-build。

-compiler-config filePath

编译器配置文件的路径。

文件必须采用特定格式。有关指导，请参阅 polyspaceroot\polyspace\configure\compiler_configuration\ 目录中的现有配置文件。有关文件内容的信息，请参阅 Create Polyspace Projects from Build Systems That Use Unsupported Compilers。

示例：-compiler-config myCompiler.xml

-no-project

选项，无需创建 Polyspace 工程即可跟踪编译系统并保存编译跟踪信息。

使用此选项可保存编译跟踪信息，以便稍后使用 -no-build 选项运行 polyspace-configure (polyspaceConfigure)。

此选项与 -compilation-database 不兼容。

-no-build

使用之前保存的编译跟踪信息创建 Polyspace 工程的选项。

要使用此选项，您必须先使用 -no-project 选项运行 polyspace-configure (polyspaceConfigure)，并保存编译跟踪信息。

如果使用此选项，则无需指定 buildCommand 参量。

当使用 -compilation-database 时，此选项将被忽略。

-no-sources

创建一个不包含源文件规格的 Polyspace 选项文件的选项。

当您打算通过其他方式指定源文件时，请使用此选项。例如，在以下情况下，您可以使用此选项：

  • 在 AUTOSAR 专用代码上运行 Polyspace。

    您要创建一个选项文件，以跟踪编译器的编译命令选项：

    -output-options-file options.txt -no-sources
    稍后，在从 ARXML 规格中提取源文件名并使用 polyspace-autosar (Polyspace Code Prover) 运行随后的 Code Prover 分析时，将此选项文件附加到后面。
    -extra-options-file options.txt

    另请参阅Run Polyspace on AUTOSAR Code Using Build Command (Polyspace Code Prover)。

  • 在 Eclipse™ 中运行 Polyspace。

    您的源文件已经在 Eclipse 工程中指定。运行 Polyspace 分析时，您需要指定一个仅包含编译选项的选项文件。

-extra-project-options polyspaceAnalysisOpts

用于后续 Polyspace 分析的选项。

创建 Polyspace 工程后，您可以更改工程中的某些默认选项。或者，您可以在跟踪编译命令时传递这些选项。标记 -extra-project-options 允许您传递其他选项。

在以空格分隔的列表中指定多个选项，例如 "-allow-negative-operand-in-shift -stubbed-pointers-are-unsafe"。

假设您必须为创建的每个 Polyspace 工程设置 -stubbed-pointers-are-unsafe 选项。无需打开每个工程并设置选项，您可以在创建 Polyspace 工程时使用此标记：

-extra-project-options "-stubbed-pointers-are-unsafe"

有关可用选项的列表，请参阅：

如果您要创建一个选项文件，而不是从编译命令创建一个 Polyspace 工程，请不要使用此标记。相反，在生成的选项文件中、单独的选项文件中或启动分析时在命令行中手动添加额外的分析选项。

-tmp-path folderPath临时文件存储的文件夹路径。
-build-trace filePath

存储编译信息的文件路径。默认值为 ./polyspace_configure_build_trace.log。

示例：-build-trace ../build_info/trace.log

-log filePath 存储 polyspace-configure 命令输出的日志文件路径。使用此选项不会抑制控制台输出。

-include-sources glob pattern

-exclude-sources glob pattern

指定 polyspace-configure (polyspaceConfigure) 在生成的工程中包括或排除哪些源文件的选项。您可以将这两个选项结合在一起使用。

如果文件路径与传递给 -include-sources 的 glob pattern 匹配，则包含源文件。

如果文件路径与传递给 -exclude-sources 的 glob pattern 匹配，则源文件将被排除。

-print-included-sources

-print-excluded-sources

打印 polyspace-configure (polyspaceConfigure) 在生成的工程中包括或排除的源文件列表的选项。您可以将这两个选项结合在一起使用。输出在单独的行中显示每个文件的完整路径。

使用此选项可对传递给 -include-sources 或 -exclude-sources 的全局模式进行故障排除。您可以查看哪些文件与传递给 -include-sources 或 -exclude-sources 的模式匹配。

-compiler-cache-path folderPath

指定 polyspace-configure 搜索或存储编译器缓存文件的文件夹路径。如果文件夹不存在，polyspace-configure 会创建它。

默认情况下，Polyspace 在以下文件夹路径下查找并存储编译器缓存：

  • Windows

    %appdata%\Mathworks\R2025a\Polyspace

  • Linux

    ~/.matlab/R2025a/Polyspace

  • Mac

    ~/Library/Application Support/MathWorks/MATLAB/R2025a/Polyspace

-no-compiler-cache

如果您不希望 Polyspace 缓存编译器配置信息或使用现有缓存来存储编译器配置，请使用此选项。

默认情况下，当您使用特定的编译器配置首次运行 polyspace-configure 时，Polyspace 会查询编译器以获取基本类型的大小、编译器宏定义以及其他编译器配置信息，然后将这些信息缓存起来。Polyspace 在后续运行 polyspace-configure 时，会重用缓存的信息来编译使用相同编译器配置的程序。

-reset-compiler-cache-entry使用此选项可查询编译器的当前配置，并刷新缓存文件中与该配置相对应的条目。缓存中的其他编译器配置项不会被更新。
-clear-compiler-cache

使用此选项可删除缓存文件中存储的所有编译器配置。

如果您还指定了编译命令或 -compilation-database，则 polyspace-configure 会计算并缓存当前运行的编译器配置信息，除非您指定了 -no-project 或 -no-compiler-cache。

-import-macro-definitions none | from-allowlist | from-source-tokens | from-compiler

通常情况下，您无需指定此选项。

Polyspace 尝试按照以下优先顺序自动确定查询编译器宏定义的最佳策略：

  1. from-compiler - Polyspace 使用本机编译器选项（例如 gcc -dm -E）来获取编译器宏定义。此策略不需要 Polyspace 跟踪您的编译，仅适用于支持列出宏定义的编译器。

  2. from-source-tokens - Polyspace 使用源代码中的所有非关键字令牌来查询编译器中的宏定义。只有当 Polyspace 能够跟踪您的编译时，此策略才可用。如果您使用选项 -compilation-database，则该策略不可用。

  3. from-allowlist - Polyspace 使用一个内部允许列表来查询编译器以获取宏定义。

如果您更喜欢手动指定宏定义，请使用此选项并添加 none 标记，然后使用选项预处理器定义 (-D) 来指定宏定义。

如果 Polyspace 使用的宏导入策略不是您期望的，请尝试手动指定此选项以解决问题。

-options-for-sources-delimiter delimCharacter

当 Polyspace 使用选项 -options-for-sources 为一个源文件生成一个选项文件时，指定用于在分析选项之间作为分隔符的字符。通常，选项 -options-for-sources 使用字符 ;（分号）作为生成的文件中分析选项之间的分隔符。

另请参阅 -options-for-sources。

这些选项主要用于调试。如果 polyspace-configure (polyspaceConfigure) 失败且 MathWorks 技术支持要求您使用该选项并提供缓存文件，请使用这些选项。从 R2020a 开始，选项 -easy-debug 提供了一种更简单的方法来提供调试信息。请参阅Contact Technical Support About Issues with Running Polyspace。

当您使用 -compilation-database 时，Polyspace 会忽略这些选项。

选项描述

-no-cache

-cache-sources（默认）

-cache-all-text

-cache-all-files

执行以下操作之一的选项：

  • -no-cache:不创建缓存

  • -cache-sources:在编译过程中临时创建的文本文件，供 polyspace-configure (polyspaceConfigure) 稍后使用。

  • -cache-all-text:缓存所有文本文件，包括源文件和头文件。

  • -cache-all-files:缓存所有文件，包括二进制文件。

通常，您会缓存编译命令创建的临时文件，以便在跟踪命令时调试问题。

-cache-path folderPath

缓存信息存储的文件夹路径。

在跟踪 Visual Studio 编译 (devenv.exe) 时，如果看到以下错误：

path is too long
尝试使用较短的路径来使用此选项，以解决错误。

示例：-cache-path ../cache

-keep-cache

-no-keep-cache（默认）

在 polyspace-configure (polyspaceConfigure) 完成执行后，保留或清理缓存信息的选项。

如果 polyspace-configure (polyspaceConfigure) 失败，您可以将此缓存信息提供给技术支持，以便进行调试。

算法

polyspace-configure 命令从编译命令（如 make）创建一个 Polyspace 工程或选项文件，大致步骤如下：

  1. 首先执行编译命令。polyspace-configure 会跟踪在此编译过程中运行的命令以及读取或写入的文件。以下一个或多个命令将作为编译器调用。例如，如果编译命令使用 GCC 编译器，则一个或多个以下命令将执行 gcc、g++ 或相关可执行文件。根据已知的编译器可执行文件的存在，polyspace-configure 从编译期间执行的所有命令中挑选出编译器调用命令。

  2. 每个编译器调用命令包含以下三个部分：编译器可执行文件、一些源文件和一些编译器选项。例如，以下命令使用编译器选项 -std 对文件 myFile.c 执行 GCC 编译器，该选项会触发基于 C++11 的编译：

    gcc -std=c++11 myFile.c
    polyspace-configure 从这些命令中读取源文件名，并直接在 Polyspace 工程或选项文件中使用它们。编译器可执行文件和编译器选项被转换为 Polyspace 分析选项。

    要确定 Polyspace 选项（例如与基本类型大小或 size_t 的底层类型相对应的选项），polyspace-configure 会在一些小型源文件上运行之前读取的编译器可执行文件以及编译器选项。根据源文件是否成功编译或出现错误，polyspace-configure 可以设置相应的 Polyspace 选项。为了确定编译器宏定义和包含路径，polyspace-configure 也会对小源代码重新调用编译器，但之后会使用略微不同的策略。

    有关可帮助确定 Polyspace 选项的源文件的简单示例，请参阅选项 size_t 的管理 (-size-t-type-is) 的参考页面。

除了编译命令外，polyspace-configure 还可以从 JSON 编译数据库创建工程或选项文件。当在编译数据库上运行 polyspace-configure 命令时，上述第一步将被省略。汇编数据库在条目中直接说明编译器调用命令，如下所示：

{
"directory": "/proj/files/
"command": "/usr/local/bin/gcc -std=c++11 -c /proj/files/myFile.c",
"file" : "/proj/files/myFile.c"
}
polyspace-configure 可以直接读取这些编译器调用命令，并继续执行剩余步骤，即对小型源文件重新调用编译器。由于跳过了编译命令的执行步骤，因此在编译数据库上运行 polyspace-configure 比在编译命令上运行 polyspace-configure 更快。但是，您有责任确保您提供的编译数据库准确反映源代码的完整编译。

版本历史记录

在 R2013b 中推出

另请参阅

主题