Frama-C 多行宏定义语法错误

Frama-C multiline macro definition syntax error

我是 Frama-C 的新手,我正在尝试正式验证包含大量多行宏定义的代码库,如下所示:

#define vector_setElement(w,x,i)                  \
  _Generic                                        \
  (                                               \
    (x),                                          \
    const int8_t    : vector_setElement_INT8   ,  \
          int8_t    : vector_setElement_INT8   ,  \
    const uint8_t   : vector_setElement_UINT8  ,  \
          uint8_t   : vector_setElement_UINT8  ,  \
    const int16_t   : vector_setElement_INT16  ,  \
          int16_t   : vector_setElement_INT16  ,  \
    const uint16_t  : vector_setElement_UINT16 ,  \
          uint16_t  : vector_setElement_UINT16 ,  \
    const int32_t   : vector_setElement_INT32  ,  \
          int32_t   : vector_setElement_INT32  ,  \
    const uint32_t  : vector_setElement_UINT32 ,  \
          uint32_t  : vector_setElement_UINT32 ,  \
    const int64_t   : vector_setElement_INT64  ,  \
          int64_t   : vector_setElement_INT64  ,  \
    const uint64_t  : vector_setElement_UINT64 ,  \
          uint64_t  : vector_setElement_UINT64 ,  \
  )                                               \
  (w, x, i)

然而,当我运行 Frama-C 使用这个宏定义时,我在使用宏定义的位置得到一个解析器语法错误。我用许多不同的多行宏定义进行了尝试,并且解析器语法错误总是发生在使用宏定义的位置。

所以,我的问题是:

Frama-C支持多行宏定义吗?如果是这样,我需要做什么来修复解析器错误?

另外,我知道 Frama-C 支持一些 C11 结构,包括 _Generic 吗?

*** 更新 - 解决方案 ***

原来_Generic是多行宏定义语法错误的原因。我认为不使用 _Generic 的多行宏定义,实际上在其他一些函数和宏调用下确实使用了它。没有 _Generic 的多行宏定义完全可以解析。

Frama-C 是 C,所以它确实支持它,但不确定 _Generics,这可能是转义在这种情况下不起作用的原因。

Frama-C 依赖于外部预处理器(编译时默认由相应的 autoconf 宏给出)来执行宏扩展,因此多行宏应该不是问题(如果是的,这将是您的预处理器的问题,而不是 Frama-C 的问题)。另一方面,_Generic 确实不在 Frama-C 目前支持的 C11 功能中。