Go to the documentation of this file.
25 throw "update: unexpected operand 0 width";
39 const exprt &new_value,
42 if(d>=designators.size())
48 if(new_value_width!=new_value_bv.size())
49 throw "convert_update_rec: unexpected new_value size";
52 for(std::size_t i=0; i<new_value_width; i++)
54 assert(offset+i<bv.size());
55 bv[offset+i]=new_value_bv[i];
61 const exprt &designator=designators[d];
63 if(designator.
id()==ID_index_designator)
65 if(type.
id()!=ID_array)
66 throw "update: index designator needs array";
69 throw "update: index designator takes one operand";
75 const exprt &size_expr = array_type.
size();
80 size_expr.
id() == ID_constant,
81 "array in update expression should be constant-sized");
84 const std::size_t size =
89 for(std::size_t i = 0; i != size; ++i)
91 std::size_t new_offset=offset+i*element_size;
94 designators, d+1, subtype, new_offset, new_value, tmp_bv);
99 for(std::size_t j=0; j<element_size; j++)
101 std::size_t idx=new_offset+j;
102 assert(idx<bv.size());
107 else if(designator.
id()==ID_member_designator)
109 const irep_idt &component_name=designator.
get(ID_component_name);
115 std::size_t struct_offset=0;
123 for(
const auto &c : components)
125 const typet &subtype = c.type();
128 if(c.get_name() == component_name)
134 struct_offset+=sub_width;
138 throw "update: failed to find struct component";
142 std::size_t new_offset=offset+struct_offset;
146 designators, d+1, new_type, new_offset, new_value, bv);
156 throw "update: failed to find union component";
164 designators, d+1, new_type, offset, new_value, bv);
167 throw "update: member designator needs struct or union";
170 throw "update: unexpected designator";
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const typet & subtype() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
std::vector< literalt > bvt
Base class for all expressions.
std::vector< componentt > componentst
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const exprt & size() const
typet & type()
Return the type of the expression.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)
const irep_idt & id() const
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...
Operator to update elements in structs and arrays.
bvt build_constant(const mp_integer &i, std::size_t width)
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
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.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bvt convert_update(const update_exprt &)
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.