Go to the documentation of this file.
36 expr.
id() == ID_byte_update_little_endian ||
37 expr.
id() == ID_byte_update_big_endian);
38 const bool little_endian = expr.
id() == ID_byte_update_little_endian;
43 std::size_t update_width=value_bv.size();
44 std::size_t byte_width=8;
46 if(update_width>bv.size())
47 update_width=bv.size();
51 const auto index = numeric_cast<mp_integer>(offset_expr);
57 if(offset+update_width>
mp_integer(bv.size()) || offset<0)
65 for(std::size_t i=0; i<update_width; i++)
66 bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
73 const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
75 for(std::size_t i=0; i<update_width; i++)
77 size_t index_op=map_op.
map_bit(offset_i+i);
78 size_t index_value=map_value.
map_bit(i);
81 index_op < bv.size(),
"bit vector index shall be within bounds");
83 index_value < value_bv.size(),
84 "bit vector index shall be within bounds");
86 bv[index_op]=value_bv[index_value];
95 for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
105 for(std::size_t bit=0; bit<update_width; bit++)
106 if(offset+bit<bv.size())
108 std::size_t bv_o=map_op.
map_bit(offset+bit);
109 std::size_t value_bv_o=map_value.
map_bit(bit);
111 bv[bv_o]=
prop.
lselect(equal, value_bv[value_bv_o], bv[bv_o]);
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
bool is_unbounded_array(const typet &type) const override
std::vector< literalt > bvt
Map bytes according to the configured endianness.
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
Base class for all expressions.
typet & type()
Return the type of the expression.
Expression classes for byte-level operators.
boolbv_widtht boolbv_width
#define PRECONDITION(CONDITION)
size_t map_bit(size_t bit) const
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Deprecated expression utility functions.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt equality(const exprt &e1, const exprt &e2)