24 error() <<
"with takes at least three operands" <<
eom;
31 error() <<
"with takes an odd number of operands" <<
eom;
51 error() <<
"unexpected operand 0 width" <<
eom;
56 prev_bv.resize(width);
60 for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
84 next_bv.resize(prev_bv.size());
86 if(type.
id()==ID_array)
88 else if(type.
id()==ID_bv ||
89 type.
id()==ID_unsignedbv ||
90 type.
id()==ID_signedbv)
92 else if(type.
id()==ID_struct)
95 else if(type.
id() == ID_struct_tag)
98 else if(type.
id()==ID_union)
100 else if(type.
id() == ID_union_tag)
103 else if(type.
id() == ID_symbol_type)
107 error() <<
"unexpected with type: " << type.
id() <<
eom;
122 error() <<
"convert_with_array called for unbounded array" <<
eom;
130 if(!size.has_value())
133 error() <<
"convert_with_array expects constant array size" <<
eom;
139 if(*size * op2_bv.size() != prev_bv.size())
142 error() <<
"convert_with_array: unexpected operand 2 width" <<
eom;
153 if(op1_value >= 0 && op1_value < *size)
155 const std::size_t offset =
156 numeric_cast_v<std::size_t>(op1_value * op2_bv.size());
158 for(std::size_t j=0; j<op2_bv.size(); j++)
159 next_bv[offset+j]=op2_bv[j];
173 const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
175 for(std::size_t j=0; j<op2_bv.size(); j++)
177 prop.
lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
194 if(op1_value<next_bv.size())
195 next_bv[numeric_cast_v<std::size_t>(op1_value)] = l;
202 for(std::size_t i=0; i<prev_bv.size(); i++)
223 const irep_idt &component_name=op1.
get(ID_component_name);
227 std::size_t offset=0;
229 for(
const auto &c : components)
231 const typet &subtype = c.type();
235 if(c.get_name() == component_name)
240 error() <<
"with/struct: component `" << component_name
241 <<
"' type does not match: " 242 << subtype.
pretty() <<
" vs. " 247 if(sub_width!=op2_bv.size())
250 error() <<
"convert_with_struct: unexpected operand op2 width" 255 for(std::size_t i=0; i<sub_width; i++)
256 next_bv[offset+i]=op2_bv[i];
275 if(next_bv.size()<op2_bv.size())
278 error() <<
"convert_with_union: unexpected operand op2 width" <<
eom;
284 for(std::size_t i=0; i<op2_bv.size(); i++)
285 next_bv[i]=op2_bv[i];
295 for(std::size_t i=0; i<op2_bv.size(); i++)
296 next_bv[map_u.
map_bit(i)]=op2_bv[map_op2.map_bit(i)];
The type of an expression, extends irept.
struct configt::ansi_ct ansi_c
virtual bvt convert_with(const exprt &expr)
literalt convert(const exprt &expr) override
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
std::vector< componentt > componentst
const componentst & components() const
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Structure type, corresponds to C style structs.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
const irep_idt & id() const
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
source_locationt source_location
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
const irep_idt & get(const irep_namet &name) const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const exprt & size() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Map bytes according to the configured endianness.
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
std::vector< exprt > operandst
const source_locationt & source_location() const
void convert_with_struct(const struct_typet &type, 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.
Base class for all expressions.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
const typet & subtype() const
std::vector< literalt > bvt