diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 8edd9abc925..2af1021ec76 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -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 enum_members; + std::vector enum_members; + enum_members.reserve(as_expr.operands().size()); // We need to determine a width, and a signedness // to obtain an 'underlying type'. @@ -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); diff --git a/src/util/c_types.h b/src/util/c_types.h index 9cf96cf1103..4d43a1aac26 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -274,6 +274,17 @@ class c_enum_typet : public type_with_subtypet typedef std::vector memberst; + c_enum_typet(typet _subtype, memberst enum_members) + : c_enum_typet(std::move(_subtype)) + { + members() = std::move(enum_members); + } + + memberst &members() + { + return reinterpret_cast(add(ID_body).get_sub()); + } + const memberst &members() const { return (const memberst &)(find(ID_body).get_sub()); diff --git a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index 6f3cb3278ca..630f4c64429 100644 --- a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -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); for(unsigned int i = 0; i < 20; ++i) { diff --git a/unit/solvers/smt2_incremental/encoding/enum_encoding.cpp b/unit/solvers/smt2_incremental/encoding/enum_encoding.cpp index 4aac95e8a5f..23d6705283a 100644 --- a/unit/solvers/smt2_incremental/encoding/enum_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/enum_encoding.cpp @@ -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) {