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)
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";
89 throw "update: failed to get array size";
95 std::size_t new_offset=offset+i*element_size;
98 designators, d+1, subtype, new_offset, new_value, tmp_bv);
103 for(std::size_t j=0; j<element_size; j++)
105 std::size_t idx=new_offset+j;
106 assert(idx<bv.size());
111 else if(designator.
id()==ID_member_designator)
113 const irep_idt &component_name=designator.
get(ID_component_name);
115 if(type.
id()==ID_struct)
120 std::size_t struct_offset=0;
128 for(struct_typet::componentst::const_iterator
129 it=components.begin();
130 it!=components.end();
133 const typet &subtype=it->type();
136 if(it->get_name()==component_name)
142 struct_offset+=sub_width;
146 throw "update: failed to find struct component";
150 std::size_t new_offset=offset+struct_offset;
154 designators, d+1, new_type, new_offset, new_value, bv);
156 else if(type.
id()==ID_union)
165 throw "update: failed to find union component";
173 designators, d+1, new_type, offset, new_value, bv);
176 throw "update: member designator needs struct or union";
179 throw "update: unexpected designator";
The type of an expression.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
boolbv_widtht boolbv_width
std::vector< componentt > componentst
const componentst & components() const
virtual bvt convert_update(const exprt &expr)
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
const irep_idt & get(const irep_namet &name) const
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::vector< exprt > operandst
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 array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
const componentt & get_component(const irep_idt &component_name) const