21 throw "byte_update takes three operands";
29 if(expr.
id()==ID_byte_update_little_endian)
31 else if(expr.
id()==ID_byte_update_big_endian)
39 std::size_t update_width=value_bv.size();
40 std::size_t byte_width=8;
42 if(update_width>bv.size())
43 update_width=bv.size();
53 if(offset+update_width>
mp_integer(bv.size()) || offset<0)
61 for(std::size_t i=0; i<update_width; i++)
71 for(std::size_t i=0; i<update_width; i++)
73 size_t index_op=map_op.map_bit(offset_i+i);
74 size_t index_value=map_value.map_bit(i);
76 assert(index_op<bv.size());
77 assert(index_value<value_bv.size());
79 bv[index_op]=value_bv[index_value];
88 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
92 equality.
lhs()=offset_expr;
99 for(std::size_t bit=0; bit<update_width; bit++)
100 if(offset+bit<bv.size())
102 std::size_t bv_o=map_op.
map_bit(offset+bit);
103 std::size_t value_bv_o=map_value.map_bit(bit);
105 bv[bv_o]=
prop.
lselect(equal, value_bv[value_bv_o], bv[bv_o]);
Maps a big-endian offset to a little-endian offset.
virtual literalt convert(const exprt &expr) override
const irep_idt & id() const
Expression classes for byte-level operators.
virtual const bvt & convert_bv(const exprt &expr)
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