Off-by-one error in naming in linking?

[martin-cs]

Some code meant to prevent compilation on inappropriate architectures (!). QUESTIONs inline... @tautschnig - you might find some of this entertaining:

$ cat cutting.c
typedef unsigned char u1;
typedef unsigned short u2;
typedef unsigned long u4;

// Correctly resolved
u2 A[( (u1)( ( (u1)1 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)1)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to A$array_size0
u4 B[( (u1)( ( (u1)15 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)15)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to B$array_size0
u2 C[( (u1)( ( (u1)11 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)11)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to C$array_size0
u4 D[( (u1)( ( (u1)4 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)4)) > ((u1)64)) ? (0) : (1) ) ) )];

$ goto-cc cutting.c -o cutting.goto -c
GCC mode
Compiling only
No. of source files: 1
No. of object files: 0
Parsing: /tmp/goto-cc-Mx5o2v/cutting.i
Converting
Type-checking cutting
Writing binary format object cutting.goto' Symbols in table: 42 Functions: 0; 0 have a body. martin@raphael:~/tmp/can-delete$ ~/working-copies/cbmc-git/src/goto-instrument/goto-instrument cutting.goto --show-symbol-table Reading GOTO program from cutting.goto'

Symbols:

Symbol......: A
Pretty name.: A
Module......: cutting
Base name...: A
Mode........: C
Type........: unsigned short int [1l]
Value.......:
Flags.......: lvalue static_lifetime
Location....: file cutting.c line 6

Symbol......: A$array_size0
Pretty name.: A$array_size0
Module......:
Base name...: A$array_size0
Mode........:
Type........: const signed long int
Value.......:
Flags.......: lvalue thread_local file_local auxiliary state_var
Location....: file cutting.c line 9

Symbol......: B
Pretty name.: B
Module......: cutting
Base name...: B
Mode........: C
Type........: unsigned long int [A$array_size0]
Value.......:
Flags.......: lvalue static_lifetime
Location....: file cutting.c line 9

Symbol......: B$array_size0
Pretty name.: B$array_size0
Module......:
Base name...: B$array_size0
Mode........:
Type........: const signed long int
Value.......:
Flags.......: lvalue thread_local file_local auxiliary state_var
Location....: file cutting.c line 12

Symbol......: C
Pretty name.: C
Module......: cutting
Base name...: C
Mode........: C
Type........: unsigned short int [B$array_size0]
Value.......:
Flags.......: lvalue static_lifetime
Location....: file cutting.c line 12

Symbol......: C$array_size0
Pretty name.: C$array_size0
Module......:
Base name...: C$array_size0
Mode........:
Type........: const signed long int
Value.......:
Flags.......: lvalue thread_local file_local auxiliary state_var
Location....: file cutting.c line 15

Symbol......: D
Pretty name.: D
Module......: cutting
Base name...: D
Mode........: C
Type........: unsigned long int [C$array_size0]
Value.......:
Flags.......: lvalue static_lifetime
Location....: file cutting.c line 15

QUESTION : why is the size of B A$array_size0, size of C B$array_size0, etc? Obviously they are synthetic variables so it doesn't matter as such but ... it is a bit surprising.

$ cat cutting-main.c
int main (int argc, char **argv)
{
return 0;
}

$ goto-cc cutting-main.c -o cutting-main.goto -c
GCC mode
Compiling only
No. of source files: 1
No. of object files: 0
Parsing: /tmp/goto-cc-J0DHT8/cutting-main.i
Converting
Type-checking cutting-main
Compiling main
Writing binary format object `cutting-main.goto'
Symbols in table: 40
Functions: 1; 1 have a body.

$ goto-cc cutting.goto cutting-main.goto -o cutting
GCC mode
Compiling and linking an executable
No. of source files: 0
No. of object files: 2
Compiling functions
Reading: cutting.goto
Reading: cutting-main.goto
file cutting.c line 9: failed to zero-initialize array of non-fixed size `A$array_size0'

QUESTION : could we give a more helpful error message, such as giving the value of A$array_size0 ?

$ cat cutting-alt.c
typedef unsigned char u1;
typedef unsigned short u2;
typedef unsigned long u4;

// Correctly resolved
u2 A[( (u1)( ( (u1)1 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)1)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to B$array_size0
u2 C[( (u1)( ( (u1)11 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)11)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to A$array_size0
u4 B[( (u1)( ( (u1)15 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)15)) > ((u1)64)) ? (0) : (1) ) ) )];

// Not resolved and set to C$array_size0
u4 D[( (u1)( ( (u1)4 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)4)) > ((u1)64)) ? (0) : (1) ) ) )];

$ goto-cc cutting-alt.c -o cutting-alt.goto -c
GCC mode
Compiling only
No. of source files: 1
No. of object files: 0
Parsing: /tmp/goto-cc-2X4lyx/cutting-alt.i
Converting
Type-checking cutting-alt
Writing binary format object `cutting-alt.goto'
Symbols in table: 41
Functions: 0; 0 have a body.

$ goto-instrument cutting.goto --list-symbols
Reading GOTO program from `cutting.goto'
A unsigned short int [1l]
A$array_size0 const signed long int
B unsigned long int [A$array_size0]
B$array_size0 const signed long int
C unsigned short int [B$array_size0]
C$array_size0 const signed long int
D unsigned long int [C$array_size0]

$ goto-instrument cutting-alt.goto --list-symbols
Reading GOTO program from `cutting-alt.goto'
A unsigned short int [1l]
B unsigned long int [C$array_size0]
B$array_size0 const signed long int
C unsigned short int [11l]
C$array_size0 const signed long int
D unsigned long int [B$array_size0]

QUESTION : Why does re-ordering two of the (independent) definitions give different results? In cutting.c why does the failure to resolve B prevent the resolution of C?