21 "with_exprt with more than 3 operands should no longer exist");
23 auto &type = expr.
type();
26 type.id() == ID_bv || type.id() == ID_unsignedbv ||
27 type.id() == ID_signedbv)
52 bv_old.size() == width,
53 "unexpected operand 0 width",
67 const exprt &new_value,
73 next_bv.resize(prev_bv.size());
75 if(type.
id()==ID_array)
78 else if(type.
id()==ID_bv ||
79 type.
id()==ID_unsignedbv ||
80 type.
id()==ID_signedbv)
85 else if(type.
id()==ID_struct)
88 else if(type.
id() == ID_struct_tag)
95 else if(type.
id()==ID_union)
97 else if(type.
id() == ID_union_tag)
112 const exprt &new_value,
119 "convert_with_array called for unbounded array",
128 "convert_with_array expects constant array size",
134 *size * new_value_bv.size() == prev_bv.size(),
135 "convert_with_array: unexpected new_value operand width",
144 if(*index_value_opt >= 0 && *index_value_opt < *size)
146 const std::size_t offset =
149 for(std::size_t j = 0; j < new_value_bv.size(); j++)
150 next_bv[offset + j] = new_value_bv[j];
164 const std::size_t offset =
167 for(std::size_t j = 0; j < new_value_bv.size(); j++)
168 next_bv[offset + j] =
169 prop.lselect(eq_lit, new_value_bv[j], prev_bv[offset + j]);
176 const exprt &new_value,
184 const irep_idt &component_name = where.
get(ID_component_name);
188 std::size_t offset=0;
190 for(
const auto &c : components)
192 const typet &subtype = c.type();
196 if(c.get_name() == component_name)
199 subtype == new_value.
type(),
200 "with/struct: component '" +
id2string(component_name) +
201 "' type does not match",
206 sub_width == new_value_bv.size(),
207 "convert_with_struct: unexpected new_value operand width",
210 for(std::size_t i=0; i<sub_width; i++)
211 next_bv[offset + i] = new_value_bv[i];
222 const exprt &new_value,
231 next_bv.size() >= new_value_bv.size(),
232 "convert_with_union: unexpected new_value operand width",
238 for(std::size_t i = 0; i < new_value_bv.size(); i++)
239 next_bv[map_u.
map_bit(i)] = new_value_bv[map_new_value.
map_bit(i)];
API to expression classes for bitvectors.
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.
const exprt & size() const
virtual bvt convert_with(const with_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
void convert_with_array(const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
bool is_unbounded_array(const typet &type) const override
void convert_with_union(const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
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_struct(const struct_typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
The type of an expression, extends irept.
Replaces a sub-range of a bit-vector operand.
Replaces a sub-range of a bit-vector operand.
Operator to update elements in structs and arrays.
const std::string & id2string(const irep_idt &d)
std::vector< literalt > bvt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#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.