Go to the documentation of this file.
26 throw "update: unexpected operand 0 width";
40 const exprt &new_value,
43 if(d>=designators.size())
49 if(new_value_width!=new_value_bv.size())
50 throw "convert_update_rec: unexpected new_value size";
53 for(std::size_t i=0; i<new_value_width; i++)
55 assert(offset+i<bv.size());
56 bv[offset+i]=new_value_bv[i];
62 const exprt &designator=designators[d];
64 if(designator.
id()==ID_index_designator)
66 if(type.
id()!=ID_array)
67 throw "update: index designator needs array";
70 throw "update: index designator takes one operand";
76 const exprt &size_expr = array_type.
size();
81 size_expr.
id() == ID_constant,
82 "array in update expression should be constant-sized");
85 const std::size_t size =
90 for(std::size_t i = 0; i != size; ++i)
92 std::size_t new_offset=offset+i*element_size;
95 designators, d+1, subtype, new_offset, new_value, tmp_bv);
100 for(std::size_t j=0; j<element_size; j++)
102 std::size_t idx=new_offset+j;
103 assert(idx<bv.size());
108 else if(designator.
id()==ID_member_designator)
110 const irep_idt &component_name=designator.
get(ID_component_name);
116 std::size_t struct_offset=0;
124 for(
const auto &c : components)
126 const typet &subtype = c.type();
129 if(c.get_name() == component_name)
135 struct_offset+=sub_width;
139 throw "update: failed to find struct component";
143 std::size_t new_offset=offset+struct_offset;
147 designators, d+1, new_type, new_offset, new_value, bv);
157 throw "update: failed to find union component";
165 designators, d+1, new_type, offset, new_value, bv);
168 throw "update: member designator needs struct or union";
171 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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
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.
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,...
virtual std::size_t boolbv_width(const typet &type) const
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.
static 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.
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.