22 throw "byte_update takes three operands";
30 if(expr.
id()==ID_byte_update_little_endian)
32 else if(expr.
id()==ID_byte_update_big_endian)
40 std::size_t update_width=value_bv.size();
41 std::size_t byte_width=8;
43 if(update_width>bv.size())
44 update_width=bv.size();
54 if(offset+update_width>
mp_integer(bv.size()) || offset<0)
62 for(std::size_t i=0; i<update_width; i++)
72 for(std::size_t i=0; i<update_width; i++)
74 size_t index_op=map_op.map_bit(offset_i+i);
75 size_t index_value=map_value.map_bit(i);
77 assert(index_op<bv.size());
78 assert(index_value<value_bv.size());
80 bv[index_op]=value_bv[index_value];
89 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
100 for(std::size_t bit=0; bit<update_width; bit++)
101 if(offset+bit<bv.size())
103 std::size_t bv_o=map_op.
map_bit(offset+bit);
104 std::size_t value_bv_o=map_value.map_bit(bit);
106 bv[bv_o]=
prop.
lselect(equal, value_bv[value_bv_o], bv[bv_o]);
literalt convert(const exprt &expr) override
boolbv_widtht boolbv_width
const irep_idt & id() const
Expression classes for byte-level operators.
virtual const bvt & convert_bv(const exprt &expr)
Map bytes according to the configured endianness.
unsigned integer2unsigned(const mp_integer &n)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
std::vector< literalt > bvt