37 "unexpected operand 0 width",
98 "convert_with_array called for unbounded array",
107 "convert_with_array expects constant array size",
113 *size * op2_bv.size() ==
prev_bv.size(),
114 "convert_with_array: unexpected operand 2 width",
123 if(*op1_value >= 0 && *op1_value < *size)
125 const std::size_t offset =
128 for(std::size_t
j=0;
j<op2_bv.size();
j++)
145 for(std::size_t
j=0;
j<op2_bv.size();
j++)
163 if(*op1_value <
next_bv.size())
196 std::size_t offset=0;
198 for(
const auto &
c : components)
200 const typet &subtype =
c.type();
204 if(
c.get_name() == component_name)
207 subtype == op2.
type(),
208 "with/struct: component '" +
id2string(component_name) +
209 "' type does not match",
215 "convert_with_struct: unexpected operand op2 width",
239 next_bv.size() >= op2_bv.size(),
240 "convert_with_union: unexpected operand op2 width",
246 for(std::size_t
i = 0;
i < op2_bv.size();
i++)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
virtual bvt convert_with(const with_exprt &expr)
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bool is_unbounded_array(const typet &type) const override
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...
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
virtual std::size_t boolbv_width(const typet &type) const
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
const std::string & id2string(const irep_idt &d)
std::vector< literalt > bvt
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.