16 const std::function<std::size_t(
const typet &)> boolbv_width,
26 std::size_t offset = 0;
28 for(
const auto &c : components)
30 const typet &subtype = c.type();
31 const std::size_t sub_width = boolbv_width(subtype);
33 if(c.get_name() == component_name)
36 subtype == expr.
type(),
37 "component type shall match the member expression type",
41 offset + sub_width <= struct_bv.size(),
42 "bitvector part corresponding to element shall be contained within the "
43 "full aggregate bitvector");
46 struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
54 "struct type shall contain component accessed by member expression",
74 "union type shall contain component accessed by member expression",
79 const std::size_t sub_width = boolbv.
boolbv_width(subtype);
85 for(std::size_t i = 0; i < sub_width; ++i)
static bvt convert_member_union(const member_exprt &expr, const bvt &union_bv, const boolbvt &boolbv, const namespacet &ns)
static bvt convert_member_struct(const member_exprt &expr, const bvt &struct_bv, const std::function< std::size_t(const typet &)> boolbv_width, const namespacet &ns)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_member(const member_exprt &expr)
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
virtual std::size_t boolbv_width(const typet &type) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & compound() const
const exprt & struct_op() const
irep_idt get_component_name() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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...
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const componentst & components() const
std::vector< componentt > componentst
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
std::vector< literalt > bvt
#define PRECONDITION(CONDITION)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.