Description
As noticed in this PR #4680 (comment)
in the example https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Global_Initialization2/main.c
the type of the array (which is declared without a length and not defined) is created with undefined length and then attached to various expressions from which the goto program is constructed. The implementation of rule 6.9.2 (https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Global_Initialization2/main.c#L15) then updates the array length of the symbol in the symbol table only, but not in the goto program. When symex takes the length from the goto program, it doesn't contain the correct length - the correct length is in the symbol table only.
CBMC version: 5.12
Operating system: ubuntu 16.04
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: the type of the array in the goto program should be set according to rule 6.9.2
What happened instead: the type is set correctly for the array entry in the symbol table but not inside code which contains the array