Provide Standard Library Headers for Polyspace Analysis
Before Polyspace® analyzes the code for bugs and run-time errors, it compiles your code. Even if the code compiles with your compiler, you can see compilation errors with Polyspace. If the error comes from a standard library function, it usually indicates that Polyspace is not using your compiler headers. To work around the errors, provide the path to your compiler headers.
If you create a Polyspace project or options file from your build command using polyspace-configure
, the header paths are
automatically added to this project or options file. Otherwise, you have to explicitly
add these paths. This topic shows how to locate the standard library headers from your
compiler. The code examples cause a compilation error that shows the location of the headers.
To locate the folder containing your C compiler system headers, compile this C code by using your compilation toolchain:
float fopen(float f); #include <stdio.h>
The code does not compile because the
fopen
declaration conflicts with the declaration insidestdio.h
. The compilation error shows the location of your compiler implementation ofstdio.h
. Your C standard library headers are all likely to be in that folder.To locate the folder containing your C++ compiler system headers, compile this C++ code by using your compilation toolchain:
The code does not compile because thenamespace std { float cin; } #include <iostream>
cin
declaration conflicts with the declaration insideiostream.h
. The compilation error shows the location of your compiler implementation ofiostream.h
. Your C++ standard library headers are all likely to be in that folder.
After you locate the path to your compiler's header files, specify the path for the Polyspace analysis. For C++ code, specify the paths to both your C and C++ headers.
In the user interface (Polyspace desktop products), add the folder to your project.
For more information, see Add Source Files for Analysis in Polyspace User Interface.
At the command line, use the flag
-I
with one of these commands:polyspace-code-prover
(Polyspace Code Prover)polyspace-code-prover-server
(Polyspace Code Prover)
For more information, see
-I
.