Go to the documentation of this file.
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");
104 op0() = std::move(e);
108 op1() = std::move(e);
112 op2() = std::move(e);
123 return base.
id() == ID_byte_update_little_endian ||
124 base.
id() == ID_byte_update_big_endian;
139 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
The type of an expression, extends irept.
An expression with three operands.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const exprt & offset() const
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Base class for all expressions.
A base class for binary expressions.
bool can_cast_expr< byte_update_exprt >(const exprt &base)
bool can_cast_expr< byte_extract_exprt >(const exprt &base)
void validate_expr(const byte_extract_exprt &value)
typet & type()
Return the type of the expression.
irep_idt byte_extract_id()
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
#define PRECONDITION(CONDITION)
const irep_idt & id() const
#define SINCE(year, month, day, msg)
irep_idt byte_update_id()
const exprt & value() const
API to expression classes.
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)