Skip to content

Improvement to c_enum_typet interface #7764

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 2 commits into from
Jun 15, 2023
Merged

Improvement to c_enum_typet interface #7764

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
607bbcc
Improved interface for c_enum_typet
Jun 15, 2023
2498769
Use new improved functions for c_enum_typet
Jun 13, 2023
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
12 changes: 5 additions & 7 deletions src/ansi-c/c_typecheck_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1270,7 +1270,8 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
// we also track min and max to find a nice base type
mp_integer value=0, min_value=0, max_value=0;

std::list<c_enum_typet::c_enum_membert> enum_members;
std::vector<c_enum_typet::c_enum_membert> enum_members;
enum_members.reserve(as_expr.operands().size());

// We need to determine a width, and a signedness
// to obtain an 'underlying type'.
Expand Down Expand Up @@ -1413,14 +1414,11 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
enum_tag_symbol.is_file_local=true;
enum_tag_symbol.base_name=base_name;

// throw in the enum members as 'body'
irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub();

for(const auto &member : enum_members)
body.push_back(member);

enum_tag_symbol.type.add_subtype() = underlying_type;

// throw in the enum members as 'body'
to_c_enum_type(enum_tag_symbol.type).members() = std::move(enum_members);

// is it in the symbol table already?
symbolt *existing_symbol = symbol_table.get_writeable(identifier);

Expand Down
3 changes: 2 additions & 1 deletion unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,8 @@ static type_symbolt make_c_enum_type_symbol(std::size_t underlying_size)
const signedbv_typet underlying_type{underlying_size};
c_enum_typet enum_type{underlying_type};

auto &members = enum_type.add(ID_body).get_sub();
auto &members = enum_type.members();
members.reserve(20);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ I might have stored 20 in a constant instead of duplicating the same magic number in 2 places.
⛏️ Also reserve is used for performance reasons. So maybe it is better to omit it in a unit test context in order to aid readability.


for(unsigned int i = 0; i < 20; ++i)
{
Expand Down
3 changes: 2 additions & 1 deletion unit/solvers/smt2_incremental/encoding/enum_encoding.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ static c_enum_typet make_c_enum_type(
{
c_enum_typet enum_type{underlying_type};

auto &members = enum_type.add(ID_body).get_sub();
auto &members = enum_type.members();
members.reserve(value_count);

for(unsigned int i = 0; i < value_count; ++i)
{
Expand Down