Go to the documentation of this file.
18 throw "update takes at three operands";
28 throw "update: unexpected operand 0 width";
42 const exprt &new_value,
45 if(type.
id() == ID_symbol_type)
47 designators, d,
ns.
follow(type), offset, new_value, bv);
49 if(d>=designators.size())
55 if(new_value_width!=new_value_bv.size())
56 throw "convert_update_rec: unexpected new_value size";
59 for(std::size_t i=0; i<new_value_width; i++)
61 assert(offset+i<bv.size());
62 bv[offset+i]=new_value_bv[i];
68 const exprt &designator=designators[d];
70 if(designator.
id()==ID_index_designator)
72 if(type.
id()!=ID_array)
73 throw "update: index designator needs array";
76 throw "update: index designator takes one operand";
87 const std::size_t size = numeric_cast_v<std::size_t>(array_type.
size());
91 for(std::size_t i = 0; i != size; ++i)
93 std::size_t new_offset=offset+i*element_size;
96 designators, d+1, subtype, new_offset, new_value, tmp_bv);
101 for(std::size_t j=0; j<element_size; j++)
103 std::size_t idx=new_offset+j;
104 assert(idx<bv.size());
109 else if(designator.
id()==ID_member_designator)
111 const irep_idt &component_name=designator.
get(ID_component_name);
113 if(type.
id()==ID_struct)
118 std::size_t struct_offset=0;
126 for(
const auto &c : components)
128 const typet &subtype = c.type();
131 if(c.get_name() == component_name)
137 struct_offset+=sub_width;
141 throw "update: failed to find struct component";
145 std::size_t new_offset=offset+struct_offset;
149 designators, d+1, new_type, new_offset, new_value, bv);
151 else if(type.
id()==ID_union)
160 throw "update: failed to find union component";
168 designators, d+1, new_type, offset, new_value, bv);
171 throw "update: member designator needs struct or union";
174 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
virtual bvt convert_update(const exprt &expr)
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)
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)
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