diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 03c15a04219..ca38d78a5f6 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/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; } diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 49fd20f4e35..155598dac6d 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/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 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( diff --git a/src/util/std_types.h b/src/util/std_types.h index 1e02a2400bb..acc03e9e703 100644 --- a/src/util/std_types.h +++ b/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,16 +1021,12 @@ 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(); @@ -1038,6 +1034,10 @@ class vector_typet:public type_with_subtypet 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.