Fix C frontend array type sync in goto program

regression/cbmc/Tentative_definition_array1/main.c

@@ -0,0 +1,26 @@
+// C standard 6.9.2, paragraph 5: a tentative definition of an array with
+// unspecified size becomes a definition with size 1.
+// This test verifies that the completed array type is propagated into
+// function bodies in the goto program, not just the symbol table.
+
+#include <assert.h>
+
+int A[];
+
+void write_A()
+{
+  A[0] = 42;
+}
+
+int read_A()
+{
+  return A[0];
+}
+
+int main()
+{
+  write_A();
+  int v = read_A();
+  assert(v == 42);
+  return 0;
+}

regression/cbmc/Tentative_definition_array1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-symex/field_sensitivity.cpp

@@ -215,15 +215,6 @@ exprt field_sensitivityt::apply(
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
-      if(l2_size.is_nil() && index.array().id() == ID_symbol)
-      {
-        // In case the array type was incomplete, attempt to retrieve it from
-        // the symbol table.
-        const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
-          to_symbol_expr(index.array()).get_identifier());
-        if(array_from_symbol_table != nullptr)
-          l2_size = to_array_type(array_from_symbol_table->type).size();
-      }
 
       if(
         l2_size.is_constant() &&

src/linking/static_lifetime_init.cpp

@@ -160,6 +160,36 @@ void static_lifetime_init(
         symbol.symbol_expr(), {}, code_type.return_type(), source_location}});
     }
   }
+
+  // C standard 6.9.2: static_lifetime_init may have completed array types
+  // (setting size from nil to a concrete value). Propagate these type updates
+  // into function bodies in the symbol table so that goto_convert produces
+  // goto programs with consistent types.
+  for(const std::string &id : symbols)
+  {
+    symbolt &symbol = symbol_table.get_writeable_ref(id);
+    if(symbol.type.id() != ID_code || symbol.value.is_nil())
+      continue;
+
+    symbol.value.visit_pre(
+      [&symbol_table](exprt &expr)
+      {
+        if(expr.id() != ID_symbol)
+          return;
+        if(expr.type().id() != ID_array)
+          return;
+        if(!to_array_type(expr.type()).size().is_nil())
+          return;
+        const auto *sym =
+          symbol_table.lookup(to_symbol_expr(expr).get_identifier());
+        if(
+          sym != nullptr && sym->type.id() == ID_array &&
+          !to_array_type(sym->type).size().is_nil())
+        {
+          expr.type() = sym->type;
+        }
+      });
+  }
 }
 
 void recreate_initialize_function(