26 expr.
id() == ID_byte_update_little_endian ||
27 expr.
id() == ID_byte_update_big_endian);
28 const bool little_endian = expr.
id() == ID_byte_update_little_endian;
33 std::size_t update_width=value_bv.size();
34 std::size_t byte_width=8;
36 if(update_width>bv.size())
37 update_width=bv.size();
41 const auto index = numeric_cast<mp_integer>(offset_expr);
47 if(offset+update_width>
mp_integer(bv.size()) || offset<0)
55 for(std::size_t i=0; i<update_width; i++)
56 bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
63 const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
65 for(std::size_t i=0; i<update_width; i++)
67 size_t index_op=map_op.map_bit(offset_i+i);
68 size_t index_value=map_value.map_bit(i);
71 index_op < bv.size(),
"bit vector index shall be within bounds");
73 index_value < value_bv.size(),
74 "bit vector index shall be within bounds");
76 bv[index_op]=value_bv[index_value];
85 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
96 for(std::size_t bit=0; bit<update_width; bit++)
97 if(offset+bit<bv.size())
99 std::size_t bv_o=map_op.
map_bit(offset+bit);
100 std::size_t value_bv_o=map_value.map_bit(bit);
102 bv[bv_o]=
prop.
lselect(equal, value_bv[value_bv_o], bv[bv_o]);
literalt convert(const exprt &expr) override
boolbv_widtht boolbv_width
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
const irep_idt & id() const
Expression classes for byte-level operators.
#define PRECONDITION(CONDITION)
Map bytes according to the configured endianness.
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::vector< literalt > bvt