Main Content

Fix Errors from Use of Polyspace Header Files

Issue

When analyzing your C/C++ source code with Polyspace®, if you do not provide the paths to your compiler headers, Polyspace uses its own version of the headers for the analysis.

In some cases, you might see compilation errors from these Polyspace headers. The error messages typically refer to one of the subfolders of polyspaceroot\polyspace\verifier\cxx\include. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b. Typically, the error message is related to a standard library function.

For instance, you might see an error on std::is_empty when analyzing this C++14 code:

#include <type_traits>

struct S final { };

bool f(void) {
    return std::is_empty<S>::value;
}
The error message states:
Error: a "final" class type cannot be used as a base class
And points to the path polyspaceroot\polyspace\verifier\cxx\include\include-libcxx\type_traits. This error happens because the implementation of std::is_empty in Polyspace header files in some cases do not allow their instantiations to use final classes.

Possible Solutions

Specify the folders containing your compiler header files for the Polyspace analysis.

If you create a Polyspace project or options file from your build command using polyspace-configure, the compiler header paths are automatically added to this project or options file. Otherwise, you have to explicitly add these paths:

For compilation with GNU® C on UNIX®-based platforms, use /usr/include. On embedded compilers, the header files are typically in a subfolder of the compiler installation folder. Examples of include folders are given for some compilers.

  • Wind River® Diab: For instance, /apps/WindRiver/Diab/5.9.4/diab/5.9.4.8/include/.

  • IAR Embedded Workbench: For instance, C:\Program Files\IAR Systems\Embedded Workbench 7.5\arm\inc.

  • Microsoft® Visual Studio®: For instance, C:\Program Files\Microsoft Visual Studio 14.0\VC\include.

Consult your compiler documentation for the path to your compiler header files. Alternatively, see Provide Standard Library Headers for Polyspace Analysis.

Related Topics