Skip to content

protect array_typet::subtype and vector_typet::subtype #7559

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 28, 2023
Merged

protect array_typet::subtype and vector_typet::subtype #7559

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_get.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/strings/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand Down Expand Up @@ -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(
Expand Down
16 changes: 8 additions & 8 deletions src/util/std_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down