On arrays vs. pointers

This post is a follow-up of bug 990. When this issue was resolved the following question arose: "Why is it so dangerous to have a global c declared as a pointer in one compilation unit and defined as an array in another one given the fact that almost anywhere an array decays as a pointer to their first element when needed?" Well the key to the answer lies in the *almost*. In fact if a is an array the associated pointer expression is &a[0] which means that it is not an lvalue on the contrary to a pointer variable p. In other words the compilation unit that sees c as a pointer can assign new values into it while it is not really expected by the compilation unit where c is defined. Worse this point cannot be checked by a compiler since there's no type at linking phase where the issue could be spotted. Take for instance the following two files: main.c

extern char* c; 
extern char f(void); 
int main () { 
  char *oldc; 
  char c1[] = "bar";  
  c = c1; 
  char test = f(); 
  c = oldc; 
  switch (test) { 
  case 'o': return 0; 
  case 'r': return 1; 
  default: return test; 
  } 
 } 

and aux.c

char c [] = "foo"; 
char f() { return c[2]; } 

gcc (Ubuntu/Linaro 4.6.3-1ubuntu5 to be precise) compiles them without any message:

gcc -o test aux.c main.c 

Yet what should be the exit status of test? One could imagine that it might be 0 if the compiler optimizes in f the fact that c is at a constant address or 1 if it uses the actual address of c (treating it effectively as pointer) when f is called. In fact on my machine the exit status is a completely arbitrary number that depends on whatever lies in the memory when test is launched:

virgile@is220177:~/tmp$ ./test 
virgile@is220177:~/tmp$ echo $? 
98 
virgile@is220177:~/tmp$ ./test 
virgile@is220177:~/tmp$ echo $? 
145 

In summary the future behavior of Frama-C that will starting from Oxygen flatly reject such code (instead of just emitting a warning) is not exceedingly pedantic. Such a discrepancy between declarations is really an important issue.