Polyspace Support for Compilers

A question comes up often: Does Polyspace^® support the compiler that I am using? Sometimes a variant of this question gets asked: Why does a static analysis tool like Polyspace need to know about a compiler? It’s not as if the tool compiles the code, creates a binary, and executes the binary to detect run-time errors. The run-time error detection does not involve executing the code at all.

The short answer is: Polyspace does not need to know about your compiler. You can provide your source code and start the analysis, but setting up a Polyspace analysis is simpler if you specify your compiler.

To understand this further, let us see how Polyspace analyzes your code.

Compilation in Polyspace

When you run Polyspace, the first step of analysis is compilation. In this step, Polyspace checks your code syntax against the C or C++ standard. For details, see Language Standard Used in Polyspace Analysis. If a file contains syntactically incorrect code, the analysis cannot proceed further. The analysis shows the syntax error just like a compiler and removes this file from consideration.

Compilers provide additional language extensions that are not found in the standard. For instance, see GCC extensions. If Polyspace knows about your compiler, the analysis can recognize these compiler-specific extensions. Otherwise, the syntax checking strictly adheres to the standard and you have to manually define these extensions for Polyspace.

For instance, GCC supports an integer scalar type  __int128 for targets that can hold 128 bits. If you use the default compilation options, Polyspace Bug Finder™ errors on this line:
const __int128 m = 3329589384618324948;

With the error:
identifier "__int128" is undefined

Simply by specifying a later version of the GCC compiler and a target that can hold 128 bits, you can avoid this error.

The setup is even easier if you already use a build command (makefile) to build your source code. You do not even have to explicitly specify a compiler. Polyspace can trace your build command and detect the compiler that you are using. Not only that, Polyspace also detects the compiler options and incorporates them in the syntax checking. For instance, if you use the GCC option std=c++14, Polyspace detects this usage and checks your code according to the C++14 standard with GCC extensions.

Compilers Directly Supported in Polyspace

As of R2019a, Polyspace directly supports these compilers:

• GCC
• Visual C++^®
• Clang
• Keil
• Diab™ (Wind River^®)
• NXP™ CodeWarrior^®
• Green Hills^®
• IAR Embedded Workbench 
• TASKING^®
• Texas Instruments™
• ARM^®

For the full list of supported compilers, see the Polyspace documentation.

Even if a compiler is not directly supported, you can still analyze your code with Polyspace. If your code is written to be portable across compilers, you are likely to have fewer errors from compiler-specific extensions. You can work around these errors with Polyspace options. For instance, you can replace a compiler-specific data type with a more recognized data type just for the purposes of Polyspace analysis (without modifying your source code).

To summarize, Polyspace supports all compilers. Some compilers are more explicitly supported compared to others. For these compilers, setting up a Polyspace analysis involves simply specifying the compiler name.