fix the constructor of element_address_exprt

The constructor now asserts that the base expression is a pointer, not an array.

Author: kroening

src/util/pointer_expr.cpp

@@ -147,13 +147,13 @@ field_address_exprt::field_address_exprt(
   set(ID_component_name, component_name);
 }
 
-element_address_exprt::element_address_exprt(exprt base, exprt index)
+element_address_exprt::element_address_exprt(const exprt &base, exprt index)
   : binary_exprt(
-      std::move(base),
+      base, // used for type, can't move
       ID_element_address,
       std::move(index),
       pointer_typet(
-        to_array_type(base.type()).element_type(),
+        to_pointer_type(base.type()).base_type(),
         to_pointer_type(base.type()).get_width()))
 {
 }

src/util/pointer_expr.h

@@ -569,7 +569,7 @@ class element_address_exprt : public binary_exprt
   /// constructor for element addresses.
   /// The base address must be a pointer to an element.
   /// The index is expected to have an integer type.
-  element_address_exprt(exprt base, exprt index);
+  element_address_exprt(const exprt &base, exprt index);
 
   const pointer_typet &type() const
   {