Merge pull request #7764 from esteffin/esteffin/improve-c-enum-constructor

Improvement to c_enum_typet interface

Author: thomasspriggs

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<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'.
@@ -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);
 

src/util/c_types.h

@@ -274,6 +274,17 @@ class c_enum_typet : public type_with_subtypet
 
   typedef std::vector<c_enum_membert> 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<memberst &>(add(ID_body).get_sub());
+  }
+
   const memberst &members() const
   {
     return (const memberst &)(find(ID_body).get_sub());

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)
   {

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)
   {