问题

当使用 Polyspace^® 分析 C/C++ 源代码时，如果您未提供编译器头文件的路径，Polyspace 将使用自己的头文件版本进行分析。

在某些情况下，您可能会遇到由这些 Polyspace 头文件引起的编译错误。错误消息通常会引用 polyspaceroot\polyspace\verifier\cxx\include 的一个子文件夹。其中，polyspaceroot 是 Polyspace 的安装文件夹，例如 C:\Program Files\Polyspace\R2025a。这类错误消息通常与标准库函数有关。

例如，在分析以下 C++14 代码时，您可能会在 std::is_empty 处看到一个错误：

#include <type_traits>

struct S final { };

bool f(void) {
    return std::is_empty<S>::value;
}

Error: a "final" class type cannot be used as a base class

可能的解决方案

指定包含您的编译器头文件的文件夹，用于 Polyspace 分析。

如果您使用 polyspace-configure 从编译命令创建 Polyspace 工程或选项文件，则编译器头文件路径会自动添加到该工程或选项文件中。否则，您必须显式添加以下路径：

在基于 UNIX^® 的平台上使用 GNU^® C 进行编译时，请使用 /usr/include。在嵌入式编译器中，头文件通常位于编译器安装文件夹的子文件夹中。以下是一些编译器的示例文件夹。

请参阅编译器文档，了解编译器头文件的路径。或者，请参阅为 Polyspace 分析提供标准库头文件。