strengthen typing of array_exprt::type

The class invariant that array expressions have array type is now enforced.

Author: Daniel Kroening

src/analyses/goto_rw.cpp

@@ -300,7 +300,7 @@ void rw_range_sett::get_objects_array(
   const range_spect &range_start,
   const range_spect &size)
 {
-  const array_typet &array_type = to_array_type(expr.type());
+  const array_typet &array_type = expr.type();
 
   auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
 

src/util/expr_initializer.cpp

@@ -122,8 +122,7 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
       // we initialize this with an empty array
 
       array_exprt value({}, array_type);
-      value.type().id(ID_array);
-      value.type().set(ID_size, from_integer(0, size_type()));
+      value.type().size() = from_integer(0, size_type());
       value.add_source_location()=source_location;
       return std::move(value);
     }

src/util/std_expr.h

@@ -1681,6 +1681,16 @@ class array_exprt : public multi_ary_exprt
     : multi_ary_exprt(ID_array, std::move(_operands), _type)
   {
   }
+
+  const array_typet &type() const
+  {
+    return static_cast<const array_typet &>(multi_ary_exprt::type());
+  }
+
+  array_typet &type()
+  {
+    return static_cast<array_typet &>(multi_ary_exprt::type());
+  }
 };
 
 template <>