Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_BYTE_OPERATORS_H
11 #define CPROVER_UTIL_BYTE_OPERATORS_H
56 return static_cast<const byte_extract_exprt &>(expr);
62 return static_cast<byte_extract_exprt &>(expr);
94 return static_cast<const byte_update_exprt &>(expr);
100 return static_cast<byte_update_exprt &>(expr);
103 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
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
Base class for all expressions.
A base class for binary expressions.
typet & type()
Return the type of the expression.
irep_idt byte_extract_id()
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
irep_idt byte_update_id()
const exprt & value() const
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)