10 #ifndef CPROVER_UTIL_BYTE_OPERATORS_H
11 #define CPROVER_UTIL_BYTE_OPERATORS_H
39 _id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
40 "byte_extract_exprt: Invalid ID");
53 return base.
id() == ID_byte_extract_little_endian ||
54 base.
id() == ID_byte_extract_big_endian;
91 _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
92 "byte_update_exprt: Invalid ID");
101 op1() = std::move(e);
105 op2() = std::move(e);
116 return base.
id() == ID_byte_update_little_endian ||
117 base.
id() == ID_byte_update_big_endian;
void validate_expr(const byte_extract_exprt &value)
irep_idt byte_extract_id()
bool can_cast_expr< byte_update_exprt >(const exprt &base)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
irep_idt byte_update_id()
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
A base class for binary expressions.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
const exprt & offset() const
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
An expression with three operands.
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)
API to expression classes.