Go to the documentation of this file.
30 std::size_t bit_field_bits = 0;
34 if(comp.get_name() == member)
37 if(comp.type().id() == ID_c_bit_field)
41 result += bit_field_bits / 8;
44 else if(comp.type().id() == ID_bool)
47 result += bit_field_bits / 8;
53 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
55 if(!sub_size.has_value())
73 for(
const auto &comp : components)
75 if(comp.get_name()==member)
79 if(!member_bits.has_value())
82 offset += *member_bits;
95 return (*bits + 7) / 8;
103 if(type.
id()==ID_array)
110 const auto size = numeric_cast<mp_integer>(
to_array_type(type).size());
111 if(!size.has_value())
114 return (*sub) * (*size);
116 else if(type.
id()==ID_vector)
126 return (*sub) * size;
128 else if(type.
id()==ID_complex)
137 else if(type.
id()==ID_struct)
144 const typet &subtype = c.type();
147 if(!sub_size.has_value())
155 else if(type.
id()==ID_union)
164 if(widest_member.has_value())
165 return widest_member->second;
169 else if(type.
id()==ID_signedbv ||
170 type.
id()==ID_unsignedbv ||
171 type.
id()==ID_fixedbv ||
172 type.
id()==ID_floatbv ||
174 type.
id()==ID_c_bool ||
175 type.
id()==ID_c_bit_field)
179 else if(type.
id()==ID_c_enum)
183 else if(type.
id()==ID_c_enum_tag)
187 else if(type.
id()==ID_bool)
191 else if(type.
id()==ID_pointer)
199 else if(type.
id() == ID_union_tag)
203 else if(type.
id() == ID_struct_tag)
207 else if(type.
id()==ID_code)
211 else if(type.
id()==ID_string)
224 if(type.
id()==ID_struct)
227 else if(type.
id()==ID_union)
240 std::size_t bit_field_bits=0;
244 if(c.get_name() == member)
247 if(c.type().id() == ID_c_bit_field)
251 const std::size_t bytes = bit_field_bits / 8;
256 else if(c.type().id() == ID_bool)
259 const std::size_t bytes = bit_field_bits / 8;
267 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
268 const typet &subtype = c.type();
270 if(!sub_size.has_value())
272 result =
plus_exprt(result, sub_size.value());
281 if(type.
id()==ID_array)
286 if(array_type.subtype().id() == ID_bool)
298 const exprt &size = array_type.size();
303 const auto size_casted =
308 else if(type.
id()==ID_vector)
313 if(vector_type.subtype().id() == ID_bool)
330 const auto size_casted =
335 else if(type.
id()==ID_complex)
344 else if(type.
id()==ID_struct)
349 std::size_t bit_field_bits=0;
353 if(c.type().id() == ID_c_bit_field)
357 const std::size_t bytes = bit_field_bits / 8;
362 else if(c.type().id() == ID_bool)
365 const std::size_t bytes = bit_field_bits / 8;
373 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
374 const typet &subtype = c.type();
376 if(!sub_size_opt.has_value())
379 result =
plus_exprt(result, sub_size_opt.value());
385 else if(type.
id()==ID_union)
396 const typet &subtype = c.type();
401 if(!sub_bits.has_value())
406 if(!sub_size_opt.has_value())
408 sub_size = sub_size_opt.value();
416 if(max_bytes<sub_bytes)
437 else if(type.
id()==ID_signedbv ||
438 type.
id()==ID_unsignedbv ||
439 type.
id()==ID_fixedbv ||
440 type.
id()==ID_floatbv ||
442 type.
id()==ID_c_bool ||
443 type.
id()==ID_c_bit_field)
446 std::size_t bytes=width/8;
451 else if(type.
id()==ID_c_enum)
455 std::size_t bytes=width/8;
460 else if(type.
id()==ID_c_enum_tag)
464 else if(type.
id()==ID_bool)
468 else if(type.
id()==ID_pointer)
475 std::size_t bytes=width/8;
480 else if(type.
id() == ID_union_tag)
484 else if(type.
id() == ID_struct_tag)
488 else if(type.
id()==ID_code)
492 else if(type.
id()==ID_string)
503 if(expr.
id()==ID_symbol)
511 else if(expr.
id()==ID_index)
516 "index into array expected, found " +
526 if(sub_size.has_value() && *sub_size > 0)
528 const auto i = numeric_cast<mp_integer>(index_expr.
index());
530 return (*o) + (*i) * (*sub_size);
536 else if(expr.
id()==ID_member)
546 if(type.
id()==ID_union)
556 else if(expr.
id()==ID_string_constant)
566 static_cast<const typet &
>(expr.
find(ID_C_c_sizeof_type));
572 auto val = numeric_cast<mp_integer>(expr);
575 !type_size.has_value() || *type_size < 0 || !val.has_value() ||
576 *val < *type_size || (*type_size == 0 && *val > 0))
584 "sizeof value does not fit size_type");
590 remainder = *val % *type_size;
595 exprt result(ID_sizeof, t);
596 result.
set(ID_type_arg, type);
609 const typet &target_type_raw,
612 if(offset_bytes == 0 && expr.
type() == target_type_raw)
616 if(expr.
type() != target_type_raw)
617 result.
type() = target_type_raw;
623 offset_bytes == 0 && expr.
type().
id() == ID_pointer &&
624 target_type_raw.
id() == ID_pointer)
631 if(!target_size_bits.has_value())
634 if(source_type.
id()==ID_struct)
642 if(!m_size_bits.has_value())
648 offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
649 offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
653 member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
656 m_offset_bits += *m_size_bits;
659 else if(source_type.
id()==ID_array)
667 elem_size_bits.has_value() && *elem_size_bits > 0 &&
668 *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
670 const mp_integer elem_size_bytes = *elem_size_bits / 8;
671 const auto offset_inside_elem = offset_bytes % elem_size_bytes;
672 const auto target_size_bytes = *target_size_bits / 8;
674 if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
687 source_type.
id() == ID_union)
694 if(!m_size_bits.has_value())
698 if(offset_bytes * 8 + *target_size_bits <= *m_size_bits)
702 member, offset_bytes, target_type_raw, ns);
714 const typet &target_type,
717 const auto offset_bytes = numeric_cast<mp_integer>(offset);
719 if(!offset_bytes.has_value())
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_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.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The type of an expression, extends irept.
optionalt< 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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Base type for structs and unions.
The trinary if-then-else operator.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Split an expression into a base object and a (byte) offset.
const irept & find(const irep_namet &name) const
The plus expression Associativity is not specified.
Base class for all expressions.
std::vector< componentt > componentst
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
bitvector_typet index_type()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
Expression classes for byte-level operators.
bool is_ssa_expr(const exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
API to expression classes for Pointers.
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
Binary multiplication Associativity is not specified.
exprt simplify_expr(exprt src, const namespacet &ns)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
nonstd::optional< T > optionalt
const constant_exprt & size() const
std::size_t get_width() const
Extract member of struct or union.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Structure type, corresponds to C style structs.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set(const irep_namet &name, const irep_idt &value)
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
A base class for relations, i.e., binary predicates whose two operands have the same type.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
Semantic type conversion.
unsignedbv_typet size_type()
A constant literal expression.
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
API to expression classes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)