diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 4538f02ee3e..dc4eb49b089 100644 --- a/src/analyses/goto_rw.cpp +++ b/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); diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 2895fce9eb0..049dc60fa5a 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -122,8 +122,7 @@ optionalt expr_initializert::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); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index ac74a5486d3..612e192c30d 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1671,11 +1671,6 @@ inline array_of_exprt &to_array_of_expr(exprt &expr) class array_exprt : public multi_ary_exprt { public: - DEPRECATED("use array_exprt(type) instead") - array_exprt() : multi_ary_exprt(ID_array) - { - } - DEPRECATED("use array_exprt(operands, type) instead") explicit array_exprt(const array_typet &_type) : multi_ary_exprt(ID_array, _type) @@ -1686,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(multi_ary_exprt::type()); + } + + array_typet &type() + { + return static_cast(multi_ary_exprt::type()); + } }; template <>