10#ifndef CPROVER_UTIL_BYTE_OPERATORS_H
11#define CPROVER_UTIL_BYTE_OPERATORS_H
35 std::size_t bits_per_byte,
40 _id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
41 "byte_extract_exprt: Invalid ID");
66 return base.
id() == ID_byte_extract_little_endian ||
67 base.
id() == ID_byte_extract_big_endian;
98 std::size_t bits_per_byte)
102 _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
103 "byte_update_exprt: Invalid ID");
110 op0() = std::move(e);
114 op1() = std::move(e);
118 op2() = std::move(e);
139 return base.
id() == ID_byte_update_little_endian ||
140 base.
id() == ID_byte_update_big_endian;
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
void validate_expr(const byte_extract_exprt &value)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
bool can_cast_expr< byte_update_exprt >(const exprt &base)
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value, std::size_t bits_per_byte)
const exprt & offset() const
void set_bits_per_byte(std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
const exprt & value() const
Base class for all expressions.
typet & type()
Return the type of the expression.
std::size_t get_size_t(const irep_idt &name) const
void set_size_t(const irep_idt &name, const std::size_t value)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
The type of an expression, extends irept.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.