Attempt to get missing array size from symbol table

In some cases, like the test in regression/cbmc/Global_Initialization2,
the array type is incomplete and changed in the symbol table after the
main function has been converted, leading to inconsistencies.
This means we can get nil instead of the size in
field_sensitivityt::apply, though the actual size is present in the
symbol table.

Author: romainbrenguier

src/goto-symex/field_sensitivity.cpp

@@ -97,10 +97,21 @@ exprt field_sensitivityt::apply(
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
       bool was_l2 = !tmp.get_level_2().empty();
+
+      exprt array_size_expr = to_array_type(l2_array.get().type()).size();
+      if(array_size_expr.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)
+          array_size_expr = to_array_type(array_from_symbol_table->type).size();
+      }
+
       if(
-        to_array_type(index.array().type()).size().id() == ID_constant &&
-        numeric_cast_v<mp_integer>(
-          to_constant_expr(to_array_type(index.array().type()).size())) <=
+        array_size_expr.id() == ID_constant &&
+        numeric_cast_v<mp_integer>(to_constant_expr(array_size_expr)) <=
           max_field_sensitive_array_size &&
         index.id() == ID_constant)
       {