为 Polyspace 分析提供标准库头文件

在 Polyspace® 分析代码中的错误和运行时错误之前，它会先编译您的代码。即使代码在您的编译器上编译通过，您仍可能在使用 Polyspace 时遇到编译错误。如果错误来自标准库函数，通常表明 Polyspace 没有使用您的编译器头文件。要解决此错误，请提供编译器头文件的路径。

如果您使用 polyspace-configure 从编译命令创建了 Polyspace 工程或选项文件，则头路径会自动添加到该工程或选项文件中。否则，您必须显式添加这些路径。本主题介绍如何从编译器中查找标准库头文件。代码示例会引发编译错误，显示头文件的位置。

  • 要定位包含 C 编译器系统头文件的文件夹，请使用您的编译工具链编译以下 C 代码：

    float fopen(float f); 
#include <stdio.h>

    该代码无法编译通过，因为 fopen 的声明与 stdio.h 中的声明冲突。编译失败的错误消息会显示编译器实现 stdio.h 的位置。您的 C 标准库头文件很可能都在该文件夹中。

  • 要定位包含 C++ 编译器系统头文件的文件夹，请使用您的编译工具链编译以下 C++ 代码：

    namespace std {
    float cin; 
}
#include <iostream>
    该代码无法编译通过，因为 cin 的声明与 iostream.h 中的声明冲突。编译失败的错误消息会显示编译器实现 iostream.h 的位置。您的 C++ 标准库头文件很可能都在该文件夹中。

找到编译器的头文件路径后，指定 Polyspace 分析的路径。对于 C++ 代码，请指定 C 和 C++ 头文件的路径。

另请参阅

主题