71 index_op < bv.size(),
"bit vector index shall be within bounds");
74 "bit vector index shall be within bounds");
84 for(std::size_t offset=0; offset<bv.size(); offset+=
byte_width)
95 if(offset+
bit<bv.size())
Expression classes for byte-level operators.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool is_unbounded_array(const typet &type) const override
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...
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & value() const
Maps a big-endian offset to a little-endian offset.
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::vector< literalt > bvt
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.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.