No error/warning on duplicate declaration of local variable

[cesaro]

The below program doesn't compile, as a local variable is declared twice

int main() {

  int a = 10;

  // gcc: main.c:140:7: error: redeclaration of 'a' with no linkage
  // cbmc: no warning or error
  int a;

  a++;

  return 0;
}

but, while gcc errors, CBMC latest develop, in Linux, doesn't raise any warning or error about it.

Sure enough, all programs that one passes to the tool should already compile, but from time to time that's not the case. Probably CBMC should error here.