10 #ifndef CPROVER_UTIL_BYTE_OPERATORS_H 11 #define CPROVER_UTIL_BYTE_OPERATORS_H 81 assert(expr.
id()==ID_byte_extract_little_endian && expr.
operands().size()==2);
88 assert(expr.
id()==ID_byte_extract_little_endian && expr.
operands().size()==2);
112 assert(expr.
id()==ID_byte_extract_big_endian && expr.
operands().size()==2);
119 assert(expr.
id()==ID_byte_extract_big_endian && expr.
operands().size()==2);
188 assert(expr.
id()==ID_byte_update_little_endian && expr.
operands().size()==3);
195 assert(expr.
id()==ID_byte_update_little_endian && expr.
operands().size()==3);
219 assert(expr.
id()==ID_byte_update_big_endian && expr.
operands().size()==3);
226 assert(expr.
id()==ID_byte_update_big_endian && expr.
operands().size()==3);
230 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
The type of an expression.
const byte_update_big_endian_exprt & to_byte_update_big_endian_expr(const exprt &expr)
const exprt & offset() const
const byte_update_little_endian_exprt & to_byte_update_little_endian_expr(const exprt &expr)
irep_idt byte_update_id()
byte_update_big_endian_exprt()
void copy_to_operands(const exprt &expr)
const exprt & value() const
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const irep_idt & id() const
A generic base class for binary expressions.
API to expression classes.
irep_idt byte_extract_id()
byte_update_little_endian_exprt()
byte_update_big_endian_exprt(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...
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
const byte_extract_little_endian_exprt & to_byte_extract_little_endian_expr(const exprt &expr)
byte_update_exprt(irep_idt _id, const typet &_type)
const byte_extract_big_endian_exprt & to_byte_extract_big_endian_expr(const exprt &expr)
Base class for all expressions.
byte_update_exprt(irep_idt _id)
byte_update_little_endian_exprt(const exprt &_op, const exprt &_offset, const exprt &_value)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)