Fix Polyspace Compilation Errors About Undefined Identifiers
Issue
Polyspace® verification fails during the compilation phase with a message about undefined identifiers.
The message indicates that Polyspace cannot find a variable definition. Therefore, it cannot identify the variable type.
Possible Cause: Missing Files
The source code you provided does not contain the variable definition. For instance, the variable is defined in an include file that Polyspace cannot find.
If you #include
-d the include file in your
source code but did not add it to your Polyspace project, you
see a previous warning:
Warning: could not find include file "my_include.h"
Solution
If the variable definition occurs in an include file, add the folder that contains the include file.
In the user interface of the 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 thepolyspace-code-prover
command.For more information, see
-I
.
Possible Cause: Unrecognized Keyword
The variable represents a keyword that your compiler recognizes but is not part of the ANSI® C standard. Therefore, Polyspace does not recognize it.
For instance, some compilers interpret __SP
as
a reference to the stack pointer.
Solution
If the variable represents a keyword that Polyspace does not recognize, replace or remove the keyword from your source code or preprocessed code.
If you remove or replace the keyword from the preprocessed code, you can avoid the compilation error while keeping your source code intact. You can do one of the following:
Replace or remove each individual unknown keyword using an analysis option. Replace the compiler-specific keyword with an equivalent keyword from the ANSI C Standard.
For information on the analysis option, see
Preprocessor definitions (-D)
.Declare the unknown keywords in a separate header file using
#define
directives. Specify that header file using an analysis option.For information on the analysis option, see
Include (-include)
. For a sample header file, see Gather Compilation Options Efficiently.
Possible Cause: Declaration Embedded in #ifdef
Statements
The variable is declared in a branch of an #ifdef
preprocessor
directive. For instance, the declaration of a variable macro_name
max_power
occurs
as follows:
#ifdef _WIN32 #define max_power 31 #endif
Your compilation toolchain might consider the macro macro_name
as
implicitly defined and execute the #ifdef
branch.
However, the Polyspace compilation might not consider the macro
as defined. Therefore, the #ifdef
branch is not
executed and the variable max_power
is not declared.
Solution
To work around the compilation error, do one of the following:
Use Target & Compiler options to directly specify your compiler. For instance, to emulate a Visual C++® compiler, set the Compiler to
visual12.0
. See Target and Compiler.Define the macro explicitly using the option
Preprocessor definitions (-D)
.
Note
If you create a Polyspace by tracing your build commands, most Target & Compiler options are automatically set.
Possible Cause: Project Created from Non-Debug Build
This can be a possible cause only if the undefined identifier occurs in an
assert
statement (or an equivalent Visual C++ macro such as ASSERT
or VERIFY
).
Typically, you come across this error in the following way. You create a Polyspace project from a build system in non-debug mode. When you run an analysis on the
project, you face a compilation error from an undefined identifier in an
assert
statement. You find that the identifier
my_identifier
is defined in a #ifndef NDEBUG
statement, for instance as
follows:
#ifndef NDEBUG int my_identifier; #endif
The C standard states that when the NDEBUG
macro
is defined, all assert statements
must be disabled.
Most IDEs define the NDEBUG
macro in their
build systems. When you build your source code in your IDE in non-debug
mode, code in a #ifndef NDEBUG
statement is removed
during preprocessing. For instance, in the preceding example, my_identifier
is
not defined. If my_identifier
occurs only in assert
statements, it is not used either, because NDEBUG
disables
assert statements. You do not have compilation errors from undefined
identifiers and your build system executes successfully.
Polyspace does not disable assert
statements
even if NDEBUG
macro is defined because the software
uses assert
statements internally to enhance verification.
When you create a Polyspace project from your build system,
if your build system defines the NDEBUG
macro,
it is also defined for your Polyspace project. Polyspace removes
code in a #ifndef NDEBUG
statement during
preprocessing, but does not disable assert
statements.
If assert
statements in your code rely on the code
in a #ifndef NDEBUG
statement, compilation errors
can occur.
In the preceding example:
The definition of
my_identifier
is removed during preprocessing.assert
statements are not disabled. Whenmy_identifier
is used in anassert
statement, you get an error because of undefined identifiermy_identifier
.
Solution
To work around this issue, create a Polyspace project from
your build system in debug mode. When you execute your build system
in debug mode, NDEBUG
is not defined. When you
create a Polyspace project from this build, NDEBUG
is
not defined for your Polyspace project.
Depending on your project settings, use the option that enables
building in debug mode. For instance, if your build system is gcc
-based,
you can define the DEBUG
macro and undefine NDEBUG
:
gcc -DDEBUG=1 -UNDEBUG *.c
Alternatively, you can disable the assert
statements in your
preprocessed code using the option Preprocessor definitions (-D)
.
However, Polyspace will not be able to emulate the assert
statements.