goto-cc fails to parse declaration with attributes before contract clauses

[archigup]

When a function declaration has GCC attributes before __CPROVER_* contract clauses, it fails to parse.

For example, take the following c file:

int test_decl(int a) __attribute__((const)) __CPROVER_requires(a != 0);

This results in:

$ goto-cc -o test.goto -c test.c 
test.c:1:1: error: syntax error before '__CPROVER_requires'
 int test_decl(int a) __attribute__((const)) __CPROVER_requires(a != 0);
PARSING ERROR

This only affects GCC attributes; C23 attributes are parsed correctly. The following works:

int test_decl(int a) [[gnu::const]] __CPROVER_requires(a != 0);

[archigup]

This can be worked around by placing the contract clauses before the attributes (through results in worse formatting).

[tautschnig]

I'll take a look - there is some risk that we can't support the desired syntax as it might cause ambiguity.