Main Content

Gather Compilation Options Efficiently

Polyspace® verification can sometimes stop in the compilation or linking phase due to the following reasons:

  • The Polyspace compiler strictly follows a C or C++ Standard (depending on your choice of compiler). See C/C++ Language Standard Used in Polyspace Analysis. If your compiler allows deviation from the Standard, the Polyspace compilation using default options cannot emulate your compiler.

  • Your compiler declares standard library functions with argument or return types different from the standard types. Unless you also provide the function definition, for efficient verification, Polyspace uses its own definitions of standard library functions, which have the usual prototype. The mismatch in types causes a linking error.

You can easily work around the compilation and standard library function errors. To work around the errors, you typically specify certain analysis options. In some cases, you might have to add a few lines to your code. For instance:

  • To emulate your compiler behavior more closely, you specify the Target & Compiler options. If you still face compilation errors, you might have to remove or replace certain unrecognized keywords using the option Preprocessor definitions (-D). However, the option allows only simple substitution of a string with another string. For more complex replacements, you might have to add #define statements to your code.

  • To avoid errors from stubbing standard library functions, you might have to #define certain Polyspace-specific macros so that Polyspace does not use its own definition of standard library functions.

Instead of adding these modifications to your original code, create a single polyspace.h  file that contains all modifications. Use the option Include (-include) to force inclusion of the polyspace.h file in all source files under verification.

Benefits of this approach include:

  • The error detection is much faster since it will be detected during compilation rather than in the link or subsequent phases.

  • There will be no need to modify original source files.

  • The file is automatically included as the very first file in the original .c files.

  • The file is reusable for other projects developed under the same environment.

Example 1. Example

This is an example of a file that can be used with the option Include (-include).

// The file may include (say) a standard include file implicitly 
// included by the cross compiler 

#include <stdlib.h> 
#include "another_file.h" 

// Workarounds for compilation errors
#define far 
#define at(x) 

// Workarounds for errors due to redefining standard library functions

#define POLYSPACE_NO_STANDARD_STUBS    // use this flag to prevent the
           //automatic stubbing of std functions 
#define __polyspace_no_sscanf 
#define __polyspace_no_fgetc 
void sscanf(int, char, char, char, char, char); 
void fgetc(void);

Related Topics