31 std::size_t bit_field_bits = 0;
35 if(comp.get_name() == member)
38 if(comp.type().id() == ID_c_bit_field)
45 else if(comp.is_boolean())
54 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
56 if(!sub_size.has_value())
74 for(
const auto &comp : components)
76 if(comp.get_name()==member)
80 if(!member_bits.has_value())
83 offset += *member_bits;
90 std::optional<mp_integer>
101 std::optional<mp_integer>
104 if(type.
id()==ID_array)
111 const auto size = numeric_cast<mp_integer>(
to_array_type(type).size());
112 if(!size.has_value())
115 return (*sub) * (*size);
117 else if(type.
id()==ID_vector)
127 return (*sub) * size;
129 else if(type.
id()==ID_complex)
138 else if(type.
id()==ID_struct)
145 const typet &subtype = c.type();
148 if(!sub_size.has_value())
156 else if(type.
id()==ID_union)
165 if(widest_member.has_value())
166 return widest_member->second;
170 else if(type.
id()==ID_signedbv ||
171 type.
id()==ID_unsignedbv ||
172 type.
id()==ID_fixedbv ||
173 type.
id()==ID_floatbv ||
175 type.
id()==ID_c_bool ||
176 type.
id()==ID_c_bit_field)
180 else if(type.
id()==ID_c_enum)
185 else if(type.
id()==ID_c_enum_tag)
189 else if(type.
id()==ID_bool)
193 else if(type.
id()==ID_pointer)
201 else if(type.
id() == ID_union_tag)
205 else if(type.
id() == ID_struct_tag)
209 else if(type.
id()==ID_code)
213 else if(type.
id()==ID_string)
226 if(compound_type.
id() == ID_struct || compound_type.
id() == ID_struct_tag)
229 compound_type.
id() == ID_struct_tag
235 else if(compound_type.
id() == ID_union || compound_type.
id() == ID_union_tag)
248 std::size_t bit_field_bits=0;
252 if(c.get_name() == member)
255 if(c.type().id() == ID_c_bit_field)
264 else if(c.is_boolean())
275 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
276 const typet &subtype = c.type();
278 if(!sub_size.has_value())
280 result =
plus_exprt(result, sub_size.value());
289 if(type.
id()==ID_array)
294 if(array_type.element_type().id() == ID_bool)
308 const exprt &size = array_type.size();
313 const auto size_casted =
318 else if(type.
id()==ID_vector)
323 if(vector_type.element_type().id() == ID_bool)
333 auto sub =
size_of_expr(vector_type.element_type(), ns);
342 const auto size_casted =
347 else if(type.
id()==ID_complex)
356 else if(type.
id()==ID_struct)
361 std::size_t bit_field_bits=0;
365 if(c.type().id() == ID_c_bit_field)
374 else if(c.is_boolean())
382 else if(c.type().get_bool(ID_C_flexible_array_member))
390 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
391 const typet &subtype = c.type();
393 if(!sub_size_opt.has_value())
396 result =
plus_exprt(result, sub_size_opt.value());
402 else if(type.
id()==ID_union)
413 const typet &subtype = c.type();
418 if(!sub_bits.has_value())
423 if(!sub_size_opt.has_value())
425 sub_size = sub_size_opt.value();
434 if(max_bytes<sub_bytes)
455 else if(type.
id()==ID_signedbv ||
456 type.
id()==ID_unsignedbv ||
457 type.
id()==ID_fixedbv ||
458 type.
id()==ID_floatbv ||
460 type.
id()==ID_c_bool ||
461 type.
id()==ID_c_bit_field)
469 else if(type.
id()==ID_c_enum)
473 else if(type.
id()==ID_c_enum_tag)
477 else if(type.
id()==ID_bool)
481 else if(type.
id()==ID_pointer)
493 else if(type.
id() == ID_union_tag)
497 else if(type.
id() == ID_struct_tag)
501 else if(type.
id()==ID_code)
505 else if(type.
id()==ID_string)
513 std::optional<mp_integer>
516 if(expr.
id()==ID_symbol)
524 else if(expr.
id()==ID_index)
529 "index into array expected, found " +
539 if(sub_size.has_value() && *sub_size > 0)
541 const auto i = numeric_cast<mp_integer>(index_expr.
index());
543 return (*o) + (*i) * (*sub_size);
549 else if(expr.
id()==ID_member)
558 if(op.
type().
id() == ID_union || op.
type().
id() == ID_union_tag)
562 op.
type().
id() == ID_struct_tag
572 else if(expr.
id()==ID_string_constant)
581 const typet &target_type_raw,
584 if(offset_bytes == 0 && expr.
type() == target_type_raw)
588 if(expr.
type() != target_type_raw)
589 result.
type() = target_type_raw;
595 offset_bytes == 0 && expr.
type().
id() == ID_pointer &&
596 target_type_raw.
id() == ID_pointer)
602 if(!target_size_bits.has_value())
605 if(expr.
type().
id() == ID_struct || expr.
type().
id() == ID_struct_tag)
608 expr.
type().
id() == ID_struct_tag
616 if(!m_size_bits.has_value())
625 m_offset_bits + *m_size_bits)
635 m_offset_bits += *m_size_bits;
638 else if(expr.
type().
id() == ID_array)
642 const auto elem_size_bits =
649 *target_size_bits <= *elem_size_bits)
655 const mp_integer index = offset_bytes / elem_size_bytes;
656 const auto offset_inside_elem = offset_bytes % elem_size_bytes;
657 const auto target_size_bytes =
661 index < array_size &&
662 offset_inside_elem + target_size_bytes <= elem_size_bytes)
668 offset_bytes / elem_size_bytes, array_type.
index_type())),
677 (expr.
type().
id() == ID_union || expr.
type().
id() == ID_union_tag))
680 expr.
type().
id() == ID_union_tag
687 if(!m_size_bits.has_value())
697 member, offset_bytes, target_type_raw, ns);
709 const typet &target_type,
712 const auto offset_bytes = numeric_cast<mp_integer>(offset);
714 if(!offset_bytes.has_value())
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet c_index_type()
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Binary multiplication Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
std::optional< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
const constant_exprt & size() const
API to expression classes for Pointers.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
bool is_ssa_expr(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.