__attribute__((__packed__)); bitfields

[tmamic]

Compiler options specified using attributes cause a parse error at parentheses after __attribute__. Cutout of code where problem occured:

typedef struct __attribute__ ((__packed__)) {
    symbol_func_type symbol_type    : 3;
    uint8_t unused                  : 1;
    symbol_data_type data_type      : 4;
}symbol_metadata;

[btj]

Yes. VeriFast doesn't currently support the __attribute__(...) syntax. It also doesn't currently support bitfields. :-(

[btj]

BTW: You can (sort of) work around these issues using the preprocessor:

typedef struct VFIGNORE(__attribute__ ((__packed__))) {
    symbol_func_type symbol_type    VFIGNORE(: 3);
    uint8_t unused                  VFIGNORE(: 1);
    symbol_data_type data_type      VFIGNORE(: 4);
}symbol_metadata;

where you define VFIGNORE as

#define VFIGNORE(x) x

when compiling and

#define VFIGNORE(x)

when verifying.