Fix C frontend array type sync in goto program

src/goto-symex/field_sensitivity.cpp

@@ -215,16 +215,7 @@ 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();
-      }
-
+      PRECONDITION(l2_size.is_not_nil());
       if(
         l2_size.is_constant() &&
         numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=

src/linking/static_lifetime_init.cpp

@@ -52,48 +52,55 @@ static std::optional<codet> static_lifetime_init(
   if(symbol.type.id() == ID_code || symbol.type.id() == ID_empty)
     return {};
 
-  if(symbol.type.id() == ID_array && to_array_type(symbol.type).size().is_nil())
+  // Get a writable reference to the symbol in case we need to update it
+  symbolt *symbol_ptr = &symbol_table.get_writeable_ref(identifier);
+
+  if(
+    symbol_ptr->type.id() == ID_array &&
+    to_array_type(symbol_ptr->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 = symbol.type;
-    writable_symbol.type.set(ID_size, from_integer(1, size_type()));
+    symbol_ptr->type.set(ID_size, from_integer(1, size_type()));
   }
 
   if(
-    (symbol.type.id() == ID_struct_tag &&
-     ns.follow_tag(to_struct_tag_type(symbol.type)).is_incomplete()) ||
-    (symbol.type.id() == ID_union_tag &&
-     ns.follow_tag(to_union_tag_type(symbol.type)).is_incomplete()))
+    (symbol_ptr->type.id() == ID_struct_tag &&
+     ns.follow_tag(to_struct_tag_type(symbol_ptr->type)).is_incomplete()) ||
+    (symbol_ptr->type.id() == ID_union_tag &&
+     ns.follow_tag(to_union_tag_type(symbol_ptr->type)).is_incomplete()))
   {
     return {}; // do not initialize
   }
 
   exprt rhs;
 
-  if((symbol.value.is_nil() && symbol.is_extern) ||
-     symbol.value.id() == ID_nondet)
+  if(
+    (symbol_ptr->value.is_nil() && symbol_ptr->is_extern) ||
+    symbol_ptr->value.id() == ID_nondet)
   {
-    if(symbol.value.get_bool(ID_C_no_nondet_initialization))
+    if(symbol_ptr->value.get_bool(ID_C_no_nondet_initialization))
       return {};
 
     // Nondet initialise if not linked, or if explicitly requested.
     // Compilers would usually complain about the unlinked symbol case.
-    const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
+    const auto nondet =
+      nondet_initializer(symbol_ptr->type, symbol_ptr->location, ns);
     CHECK_RETURN(nondet.has_value());
     rhs = *nondet;
   }
-  else if(symbol.value.is_nil())
+  else if(symbol_ptr->value.is_nil())
   {
-    const auto zero = zero_initializer(symbol.type, symbol.location, ns);
+    const auto zero =
+      zero_initializer(symbol_ptr->type, symbol_ptr->location, ns);
     CHECK_RETURN(zero.has_value());
     rhs = *zero;
   }
   else
-    rhs = symbol.value;
+    rhs = symbol_ptr->value;
 
-  return code_frontend_assignt{symbol.symbol_expr(), rhs, symbol.location};
+  return code_frontend_assignt{
+    symbol_ptr->symbol_expr(), rhs, symbol_ptr->location};
 }
 
 void static_lifetime_init(