Fix Polyspace Compilation Errors Related to GNU Compiler

If you choose gnu for the option Compilation toolchain (Static analysis), you can encounter this issue.

Issue

The Polyspace^® analysis stops with a compilation error.

Cause

You are using certain advanced compiler-specific extensions that Polyspace does not support.

Solution

For easier portability of your code, avoid using the extensions.

If you want to use the extensions and still analyze your code, wrap the unsupported extensions in a preprocessor directive. For instance:

#ifdef POLYSPACE
    // Supported syntax
#else
    // Unsupported syntax
#endif

Do not define the macro POLYSPACE for regular compilation but for Polyspace analysis, enter POLYSPACE for the option Preprocessor definitions (-D).

If the compilation error is related to assembly language code, use the option -asm-begin -asm-end.

Note that Polyspace does not support the following features of GNU compilers.

• GNU^® compilers versions 4.7 and later:

  • Nested functions.

    For instance, the function bar is nested in function foo:

    int foo (int a, int b)
    {
      int bar (int c) { return c * c; }
    
      return bar (a) + bar (b);
    }

  • Binary operations with vector types where one operand uses the shorthand notation for uniform vectors.

    For instance, in the addition operation, 2+a, 2 is used as a shorthand notation for {2,2,2,2}.

    typedef int v4si __attribute__ ((vector_size (16)));
    v4si res, a = {1,2,3,4};
    
    res = 2 + a;  /* means {2,2,2,2} + a  */

  • Forward declaration of function parameters.

    For instance, the parameter len is forward declared:

    void func (int len; char data[len][len], int len)
    {
      /* … */
    }

  • Complex integer data types.

    However, complex floating point data types are supported.

  • Initialization of structures with flexible array members using an initialization list.

    For instance, the structure S has a flexible array member tab. A variable of type S is directly initialized with an initialization list.

    struct S {
        int x;
        int tab[];            /* flexible array member - not supported */
    };
    struct S s = { 0, 1, 2} ;

    You see a warning during analysis and a red check in the results when you dereference, for instance, s.tab[1].

  • 128-bit variables.

    Polyspace cannot analyze this data type semantically. Bug Finder allows use of 128-bit data types, but Code Prover shows a compilation error if you use such a data type, for instance, the GCC extension __float128.

• GNU compilers version 7.x:

  • Type names _FloatN and _FloatNx are not semantically supported. The analysis treats them as type float, double, or long double.

  • Constants of type _FloatN or _FloatNx with suffixes fN, FN, or fNx, such as 1.2f123 or 2.3F64x are not supported.