37 if(comp.type().id()==ID_c_bit_field)
49 const typet &subtype=comp.type();
68 for(struct_typet::componentst::const_iterator
69 it=components.begin();
70 it!=components.end() && offsets->second!=-1;
73 if(it->get_name()==member)
77 return offsets->second;
88 for(
const auto &comp : components)
90 if(comp.get_name()==member)
118 if(type.
id()==ID_array)
135 else if(type.
id()==ID_vector)
152 else if(type.
id()==ID_complex)
160 else if(type.
id()==ID_struct)
168 for(struct_typet::componentst::const_iterator
169 it=components.begin();
170 it!=components.end();
173 const typet &subtype=it->type();
182 else if(type.
id()==ID_union)
192 for(union_typet::componentst::const_iterator
193 it=components.begin();
194 it!=components.end();
197 const typet &subtype=it->type();
207 else if(type.
id()==ID_signedbv ||
208 type.
id()==ID_unsignedbv ||
209 type.
id()==ID_fixedbv ||
210 type.
id()==ID_floatbv ||
212 type.
id()==ID_c_bool ||
213 type.
id()==ID_c_bit_field)
217 else if(type.
id()==ID_c_enum)
221 else if(type.
id()==ID_c_enum_tag)
225 else if(type.
id()==ID_bool)
229 else if(type.
id()==ID_pointer)
237 else if(type.
id()==ID_symbol)
241 else if(type.
id() == ID_union_tag)
245 else if(type.
id() == ID_struct_tag)
249 else if(type.
id()==ID_code)
253 else if(type.
id()==ID_string)
267 if(type.
id()==ID_struct)
270 else if(type.
id()==ID_union)
284 std::size_t bit_field_bits=0;
286 for(struct_typet::componentst::const_iterator
287 it=components.begin();
288 it!=components.end();
291 if(it->get_name()==member)
294 if(it->type().id()==ID_c_bit_field)
298 const std::size_t bytes = bit_field_bits / 8;
305 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
306 const typet &subtype=it->type();
323 if(type.
id()==ID_array)
343 else if(type.
id()==ID_vector)
363 else if(type.
id()==ID_complex)
376 else if(type.
id()==ID_struct)
383 std::size_t bit_field_bits=0;
385 for(struct_typet::componentst::const_iterator
386 it=components.begin();
387 it!=components.end();
390 if(it->type().id()==ID_c_bit_field)
394 const std::size_t bytes = bit_field_bits / 8;
401 bit_field_bits == 0,
"padding ensures offset at byte boundaries");
402 const typet &subtype=it->type();
415 else if(type.
id()==ID_union)
426 for(union_typet::componentst::const_iterator
427 it=components.begin();
428 it!=components.end();
431 const typet &subtype=it->type();
450 if(max_bytes<sub_bytes)
471 else if(type.
id()==ID_signedbv ||
472 type.
id()==ID_unsignedbv ||
473 type.
id()==ID_fixedbv ||
474 type.
id()==ID_floatbv ||
476 type.
id()==ID_c_bool ||
477 type.
id()==ID_c_bit_field)
480 std::size_t bytes=width/8;
485 else if(type.
id()==ID_c_enum)
488 std::size_t bytes=width/8;
493 else if(type.
id()==ID_c_enum_tag)
497 else if(type.
id()==ID_bool)
501 else if(type.
id()==ID_pointer)
508 std::size_t bytes=width/8;
513 else if(type.
id()==ID_symbol)
517 else if(type.
id() == ID_union_tag)
521 else if(type.
id() == ID_struct_tag)
525 else if(type.
id()==ID_code)
529 else if(type.
id()==ID_string)
541 if(expr.
id()==ID_symbol)
549 else if(expr.
id()==ID_index)
554 array_type.
id()==ID_array,
555 "index into array expected, found "+array_type.
id_string());
572 else if(expr.
id()==ID_member)
582 if(type.
id()==ID_union)
589 else if(expr.
id()==ID_string_constant)
600 static_cast<const typet &
>(expr.
find(ID_C_c_sizeof_type));
610 (type_size==0 && val>0))
616 "sizeof value does not fit size_type");
621 remainder=val%type_size;
626 exprt result(ID_sizeof, t);
627 result.
set(ID_type_arg, type);
643 const typet &target_type_raw,
647 const typet &target_type=ns.
follow(target_type_raw);
649 if(offset==0 && source_type==target_type)
652 if(source_type.
id()==ID_struct)
657 while(offsets->first<components.size() &&
658 offsets->second!=-1 &&
659 offsets->second<=offset)
663 if((offsets->first+1)==components.size() || offset<nextit->second)
669 components[offsets->first].get_name(),
670 components[offsets->first].
type());
673 result, offset-offsets->second, target_type, ns);
679 else if(source_type.
id()==ID_array)
688 if(cellidx < 0 || !cellidx.is_long())
690 offset=offset%elem_size;
701 const typet &target_type,
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
const struct_typet & type
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
A generic base class for relations, i.e., binary predicates.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
member_offset_iterator(const struct_typet &_type, const namespacet &_ns)
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
const componentst & components() const
The trinary if-then-else operator.
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
A constant literal expression.
bool get_bool(const irep_namet &name) const
const typet & follow_tag(const union_tag_typet &) const
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
API to expression classes.
const exprt & size() const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
const exprt & size() const
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
Base type of C structs and unions, and C++ classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const exprt & struct_op() const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const exprt & get_original_expr() const
irep_idt get_component_name() const
bool is_ssa_expr(const exprt &expr)
member_offset_iterator & operator++()
const std::string & id_string() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
mp_integer member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
bool simplify(exprt &expr, const namespacet &ns)