30 std::pair<cachet::iterator, bool> cache_result=
31 cache.insert(std::pair<typet, entryt>(type,
entryt()));
33 entryt &entry=cache_result.first->second;
35 if(!cache_result.second)
42 if(type_id==ID_struct)
48 entry.
members.resize(components.size());
50 for(std::size_t i=0; i<entry.
members.size(); i++)
52 std::size_t sub_width=
operator()(components[i].type());
54 entry.
members[i].width=sub_width;
60 else if(type_id==ID_union)
65 entry.
members.resize(components.size());
67 std::size_t max_width=0;
69 for(std::size_t i=0; i<entry.
members.size(); i++)
71 std::size_t sub_width=
operator()(components[i].type());
72 entry.
members[i].width=sub_width;
73 max_width=std::max(max_width, sub_width);
78 else if(type_id==ID_bool)
80 else if(type_id==ID_c_bool)
84 else if(type_id==ID_signedbv)
88 else if(type_id==ID_unsignedbv)
92 else if(type_id==ID_floatbv)
96 else if(type_id==ID_fixedbv)
100 else if(type_id==ID_bv)
104 else if(type_id==ID_verilog_signedbv ||
105 type_id==ID_verilog_unsignedbv)
110 size > 0,
"verilog bitvector width shall be greater than zero");
113 else if(type_id==ID_range)
126 else if(type_id==ID_array)
131 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
133 if(!array_size.has_value())
144 entry.
total_width = numeric_cast_v<std::size_t>(total);
147 else if(type_id==ID_vector)
152 const auto vector_size = numeric_cast_v<mp_integer>(vector_type.
size());
155 if(total > (1 << 30))
158 entry.
total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
160 else if(type_id==ID_complex)
163 entry.
total_width = numeric_cast_v<std::size_t>(2 * sub_width);
165 else if(type_id==ID_code)
168 else if(type_id==ID_enumeration)
175 else if(type_id==ID_c_enum)
181 else if(type_id==ID_incomplete_c_enum)
185 else if(type_id==ID_pointer)
186 entry.
total_width = type_checked_cast<pointer_typet>(type).get_width();
187 else if(type_id == ID_symbol_type)
189 else if(type_id==ID_struct_tag)
191 else if(type_id==ID_union_tag)
193 else if(type_id==ID_c_enum_tag)
195 else if(type_id==ID_c_bit_field)
199 else if(type_id==ID_string)
201 else if(type_id != ID_empty)
The type of an expression, extends irept.
const mp_integer string2integer(const std::string &n, unsigned base)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
std::vector< componentt > componentst
const componentst & components() const
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
const irep_idt & id() const
const membert & get_member(const struct_typet &type, const irep_idt &member) const
std::size_t operator()(const typet &type) const
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const exprt & size() const
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const exprt & size() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
boolbv_widtht(const namespacet &_ns)
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
std::vector< membert > members
const irept::subt & elements() const
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const std::string & get_string(const irep_namet &name) const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
std::size_t get_size_t(const irep_namet &name) const
const entryt & get_entry(const typet &type) const