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.