修复与 GNU 编译器相关的 Polyspace 编译错误

如果您为编译工具链(静态分析) 选项选择 gnu，则可能会遇到此问题。

问题

Polyspace^® 分析因编译错误而停止。

原因

您正在使用 Polyspace 不支持的某些特定于编译器的高级扩展。

解决方案

为了更轻松地移植代码，请避免使用这些扩展。

如果您要使用这些扩展并仍然分析代码，请将不支持的扩展包装在预处理器指令中。例如：

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

对于常规编译，请不要定义宏 POLYSPACE，但对于 Polyspace 分析，请为预处理器定义 (-D) 选项输入 POLYSPACE。

如果编译错误与汇编语言代码有关，请使用 -asm-begin -asm-end 选项。

请注意，Polyspace 不支持 GNU 编译器的以下功能。

GNU^® 编译器版本 4.7 及更高版本：
- 嵌套函数。
  例如，在函数 foo 中嵌套函数 bar：
```
int foo (int a, int b)
{
  int bar (int c) { return c * c; }

  return bar (a) + bar (b);
}
```
- 对向量类型执行的二元运算，其中一个操作数使用了简化形式表示等值向量。
  例如，在加法运算 2+a 中，2 用作 {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  */
```
- 函数参数的前向声明。
  例如，对参数 len 进行前向声明：
```
void func (int len; char data[len][len], int len)
{
  /* … */
}
```
- 复整数数据类型。
  但是，支持复杂的浮点数据类型。
- 使用初始化列表初始化具有灵活数组成员的结构体。
  例如，结构 S 具有一个灵活数组成员 tab。直接使用初始化列表初始化 S 类型的变量。
```
struct S {
    int x;
    int tab[];            /* flexible array member - not supported */
};
struct S s = { 0, 1, 2} ;
```
  分析过程中您会看到一条警告，解引用时会在结果中看到红色检查，例如 s.tab[1]。
- 128 位变量。
  Polyspace 无法从语义方面分析此数据类型。Bug Finder 允许使用 128 位数据类型，但是如果您使用此种数据类型（例如 GCC 扩展 __float128），则 Code Prover 会显示编译错误。
GNU 编译器版本 7.x：
- 语义上不支持类型名称 _FloatN 和 _FloatNx。分析会将它们视为 float、double 或 long double 类型。
- 不支持 _FloatN 或 _FloatNx 类型且带有后缀 fN、FN 或 fNx 的常量，例如 1.2f123 或 2.3F64x。