我是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依靠外部预处理器(默认由编译时相应的autoconf
宏给定)执行宏扩展,因此多行宏应该不是问题(如果存在,这将是一个问题)您的预处理器,而不是Frama-C)。另一方面,现在_Generic
确实不在Frama-C支持的C11功能之中。
关于frama-c - Frama-C多行宏定义语法错误,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/50957918/