Merge pull request #7559 from diffblue/array_vector_subtype

protect array_typet::subtype and vector_typet::subtype

Author: tautschnig

src/solvers/flattening/boolbv_get.cpp

@@ -339,7 +339,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
         {
           if(value.is_nil())
             values[*index_mpint] =
-              exprt(ID_unknown, to_array_type(type).subtype());
+              exprt(ID_unknown, to_array_type(type).element_type());
           else
             values[*index_mpint] = value;
         }

src/solvers/strings/string_refinement.cpp

@@ -927,7 +927,7 @@ void string_refinementt::add_lemma(
     {
       it.mutate() = array_of_exprt(
         from_integer(
-          CHARACTER_FOR_UNKNOWN, to_array_type(it->type()).subtype()),
+          CHARACTER_FOR_UNKNOWN, to_array_type(it->type()).element_type()),
         to_array_type(it->type()));
       it.next_sibling_or_parent();
     }
@@ -1032,7 +1032,7 @@ static optionalt<exprt> get_array(
   }
 
   const exprt arr_val = simplify_expr(super_get(arr), ns);
-  const typet char_type = to_array_type(arr.type()).subtype();
+  const typet char_type = to_array_type(arr.type()).element_type();
   const typet &index_type = size.value().type();
 
   if(

src/util/std_types.h

@@ -780,16 +780,12 @@ class array_typet:public type_with_subtypet
   }
 
   /// The type of the elements of the array.
-  /// This method is preferred over .subtype(),
-  /// which will eventually be deprecated.
   const typet &element_type() const
   {
     return subtype();
   }
 
   /// The type of the elements of the array.
-  /// This method is preferred over .subtype(),
-  /// which will eventually be deprecated.
   typet &element_type()
   {
     return subtype();
@@ -822,6 +818,10 @@ class array_typet:public type_with_subtypet
   static void check(
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT);
+
+protected:
+  // Use element_type() instead
+  using type_with_subtypet::subtype;
 };
 
 /// Check whether a reference to a typet is a \ref array_typet.
@@ -1021,23 +1021,23 @@ class vector_typet:public type_with_subtypet
   }
 
   /// The type of the elements of the vector.
-  /// This method is preferred over .subtype(),
-  /// which will eventually be deprecated.
   const typet &element_type() const
   {
     return subtype();
   }
 
   /// The type of the elements of the vector.
-  /// This method is preferred over .subtype(),
-  /// which will eventually be deprecated.
   typet &element_type()
   {
     return subtype();
   }
 
   const constant_exprt &size() const;
   constant_exprt &size();
+
+protected:
+  // Use element_type() instead
+  using type_with_subtypet::subtype;
 };
 
 /// Check whether a reference to a typet is a \ref vector_typet.