Type mismatch for extern array declaration

[danpoe]

// err1.c
extern int tbl2[];
int* tbl1 = tbl2;

// err2.c
int tbl2[2];
void main( void )
{
}

cbmc --show-vcc err1.c err2.c

Yields the following error:

CBMC version 5.5 64-bit x86_64 windows
Parsing err1.c
Parsing err2.c
Converting
Type-checking err1
Type-checking err2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
file err2.c line 1: value_sett::assign type mismatch: rhs.type():
...

[kroening]

Added as regression/cbmc/Linking5

[danpoe]

I'm unsure what the correct fix for this would be. The problematic code portion in the goto program is the following in __CPROVER_initialize():

...
tbl2 = tbl1;      (types: int *, int[])
tbl1 = { 0, 0 };  (types: int[2], int[2])
...

The goto symex seems to use the type of the first occurence of tbl1 (int[]) also for the second occurence of tbl1 (caching?) which then leads to a type mismatch in the value set analysis.

Should

(1) the goto symex avoid the caching and always take the type from the symbol occurence in the code?

(2) the value set analysis be able to handle assignment statements between int[] and int[2]?

(3) the linking stage adapt the code such that different occurences of the same symbol have the same type?