Search code examples
frama-c

Frama-C multiline macro definition syntax error

I am new to Frama-C and I am trying to formally verify a code base that contains a significant number of multiline macro definitions which look like this:

#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)

However when I run Frama-C on the use of this macro definition, I get a parser syntax error at the location of the use of the macro definition. I tried this with many different multiline macro definitions and a parser syntax error always occurs at the location of the use of the macro definition.

So, my questions are:

Does Frama-C support multiline macro definitions? If so, what do I need to do to fix the parser errors?

Also, I know Frama-C supports some C11 constructs, does that include _Generic?

*** Update - Solution ***

It turns out _Generic is the reason for the syntax errors with multiline macro definitions. Multiline macro definitions that I thought do not use _Generic, in fact do use it beneath a few other function and macro calls. Multiline macro definitions without _Generic parse completely fine.

Solution

  • Frama-C relies on an external pre-processor (default is given by the corresponding autoconf macro at compile time) to perform macro expansions, thus multi-line macros should not be a problem (and if it were, this would be an issue with your pre-processor, not with Frama-C). On the other hand, _Generic is indeed not among C11 features that Frama-C does support at this time.