C front-end: ensure array type updates are consistent

We must not end up in a situation where the symbol's array type is
different from the type applied to symbol expressions in code. With the
previous approach, support-function generation would alter the type
after typechecking of code had already been completed.

Fixes: #7608

Author: tautschnig

regression/cbmc/extern6/main.c

@@ -0,0 +1,12 @@
+extern int stuff[];
+
+extern int a[];
+int a[] = {1, 2, 3};
+
+int main()
+{
+  unsigned char idx;
+  long val = *(long *)(stuff + idx);
+  __CPROVER_assert(val == 13, "compare");
+  return 0;
+}

regression/cbmc/extern6/test.desc

@@ -0,0 +1,9 @@
+CORE new-smt-backend
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^Invariant check failed

src/ansi-c/c_typecheck_base.cpp

@@ -314,7 +314,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
 
   if(
     final_old.id() == ID_array &&
-    to_array_type(final_old).size().is_not_nil() &&
+    to_array_type(final_old).size().is_not_nil() && !old_symbol.is_weak &&
     initial_new.id() == ID_array &&
     to_array_type(initial_new).size().is_nil() &&
     to_array_type(final_old).element_type() ==
@@ -504,7 +504,8 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
   if(final_old!=final_new)
   {
     if(
-      final_old.id() == ID_array && to_array_type(final_old).size().is_nil() &&
+      final_old.id() == ID_array &&
+      (to_array_type(final_old).size().is_nil() || old_symbol.is_weak) &&
       final_new.id() == ID_array &&
       to_array_type(final_new).size().is_not_nil() &&
       to_array_type(final_old).element_type() ==

src/ansi-c/c_typecheck_initializer.cpp

@@ -249,6 +249,15 @@ void c_typecheck_baset::do_initializer(symbolt &symbol)
     if(!symbol.is_macro && symbol.type != symbol.value.type())
       symbol.type = symbol.value.type();
   }
+  else if(
+    symbol.type.id() == ID_array && to_array_type(symbol.type).size().is_nil())
+  {
+    // C standard 6.9.2, paragraph 5
+    // adjust the type to an array of size 1, but mark as weak so that linking
+    // can change that
+    to_array_type(symbol.type).size() = from_integer(1, size_type());
+    symbol.is_weak = true;
+  }
 
   if(symbol.is_macro)
     make_constant(symbol.value);

src/linking/static_lifetime_init.cpp

@@ -50,14 +50,9 @@ static optionalt<codet> static_lifetime_init(
   if(type.id() == ID_code || type.id() == ID_empty)
     return {};
 
-  if(type.id() == ID_array && to_array_type(type).size().is_nil())
-  {
-    // C standard 6.9.2, paragraph 5
-    // adjust the type to an array of size 1
-    symbolt &writable_symbol = symbol_table.get_writeable_ref(identifier);
-    writable_symbol.type = type;
-    writable_symbol.type.set(ID_size, from_integer(1, size_type()));
-  }
+  DATA_INVARIANT(
+    type.id() != ID_array || to_array_type(type).size().is_not_nil(),
+    "arrays must have a size");
 
   if(
     (type.id() == ID_struct || type.id() == ID_union) &&