Unexpected behaviour when defining functions wrongly

[ArmborstL]

At first glance, the following example looks fine, but VerCors rejects the assert:

#include<stdbool.h>

//@ ghost bool b() = true;

int main() {
  //@ assert b();
}

The issue is that ghost should be pure.
Now, it seems that VerCors parses bool b() = true using the rules for a global variable declaration like int x = 2, mixed with rules for a method forward declaration bool b();. Because VerCors does not currently support global variable initializers, the =true is silently dropped, hiding the issue.
We probably want to disallow mixing forward declarations with assigning a value. There are (at least) two possibilities how:

1. change the grammar: in LangCParser's directDeclarator, remove the cases relating to parentheses, and instead add explicit cases to externalDeclaration to handle forward declarations. This would also impact other cases of parentheses in declarators, such as method arguments that are function pointers (int myMeth(double(*givenFun(int,float)))). However, the latter are currently not supported by the parser anyway (we disallowed the '(' declarator ')' case). It would also mean further deviations from the "official" ANTLR C grammar.
2. leave the grammar and handle it in the translation, e.g. CToCol. This would also allow to give a more specific error message ("you cannot combine A and B"), rather than a generic "VerCors cannot parse this" error.