Go to the documentation of this file.
35 "unexpected operand 0 width",
39 prev_bv.resize(width);
43 for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
62 next_bv.resize(prev_bv.size());
64 if(type.
id()==ID_array)
66 else if(type.
id()==ID_bv ||
67 type.
id()==ID_unsignedbv ||
68 type.
id()==ID_signedbv)
70 else if(type.
id()==ID_struct)
73 else if(type.
id() == ID_struct_tag)
76 else if(type.
id()==ID_union)
78 else if(type.
id() == ID_union_tag)
96 "convert_with_array called for unbounded array",
101 const auto size = numeric_cast<mp_integer>(array_size);
105 "convert_with_array expects constant array size",
111 *size * op2_bv.size() == prev_bv.size(),
112 "convert_with_array: unexpected operand 2 width",
116 if(
const auto op1_value = numeric_cast<mp_integer>(op1))
121 if(*op1_value >= 0 && *op1_value < *size)
123 const std::size_t offset =
124 numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
126 for(std::size_t j=0; j<op2_bv.size(); j++)
127 next_bv[offset+j]=op2_bv[j];
141 const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
143 for(std::size_t j=0; j<op2_bv.size(); j++)
145 prop.
lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
157 if(
const auto op1_value = numeric_cast<mp_integer>(op1))
161 if(*op1_value < next_bv.size())
162 next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
169 for(std::size_t i=0; i<prev_bv.size(); i++)
190 const irep_idt &component_name=op1.
get(ID_component_name);
194 std::size_t offset=0;
196 for(
const auto &c : components)
198 const typet &subtype = c.type();
202 if(c.get_name() == component_name)
205 subtype == op2.
type(),
206 "with/struct: component '" +
id2string(component_name) +
207 "' type does not match",
212 sub_width == op2_bv.size(),
213 "convert_with_struct: unexpected operand op2 width",
216 for(std::size_t i=0; i<sub_width; i++)
217 next_bv[offset+i]=op2_bv[i];
237 next_bv.size() >= op2_bv.size(),
238 "convert_with_union: unexpected operand op2 width",
243 for(std::size_t i=0; i<op2_bv.size(); i++)
244 next_bv[i]=op2_bv[i];
254 for(std::size_t i=0; i<op2_bv.size(); i++)
Operator to update elements in structs and arrays.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool is_unbounded_array(const typet &type) const override
The type of an expression, extends irept.
std::vector< literalt > bvt
Map bytes according to the configured endianness.
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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.
struct configt::ansi_ct ansi_c
const exprt & size() const
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
void conversion_failed(const exprt &expr, bvt &bv)
const std::string & id2string(const irep_idt &d)
size_t map_bit(size_t bit) const
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
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...
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Structure type, corresponds to C style structs.
const irep_idt & get(const irep_namet &name) const
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
API to expression classes.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bvt convert_with(const with_exprt &expr)