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

@@ -96,11 +96,22 @@ exprt field_sensitivityt::apply(
       l2_index.simplify(ns);
       auto l2_array = state.rename(index.array(), ns);
       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(l2_array.get().type()).size().id() == ID_constant &&
-        numeric_cast_v<mp_integer>(to_constant_expr(to_array_type(
-          l2_array.get().type()).size()))
-        <= max_field_sensitive_array_size &&
+        array_size_expr.id() == ID_constant &&
+        numeric_cast_v<mp_integer>(to_constant_expr(array_size_expr))
+          <= max_field_sensitive_array_size &&
         l2_index.get().id() == ID_constant)
       {
         // place the entire index expression, not just the array operand, in an
@@ -324,8 +335,9 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
   if(
     expr.type().id() == ID_array &&
     to_array_type(expr.type()).size().id() == ID_constant &&
-    numeric_cast_v<mp_integer>(to_constant_expr(to_array_type(expr.type()).size()))
-      <= max_field_sensitive_array_size)
+    numeric_cast_v<mp_integer>(
+      to_constant_expr(to_array_type(expr.type()).size()))
+    <= max_field_sensitive_array_size)
   {
     return true;
   }