CBMC
|
Expression classes for byte-level operators. More...
Go to the source code of this file.
Classes | |
class | byte_extract_exprt |
Expression of type type extracted from some object op starting at position offset (given in number of bytes). More... | |
class | byte_update_exprt |
Expression corresponding to op() where the bytes starting at position offset (given in number of bytes) have been updated with value . More... | |
Functions | |
template<> | |
bool | can_cast_expr< byte_extract_exprt > (const exprt &base) |
const byte_extract_exprt & | to_byte_extract_expr (const exprt &expr) |
byte_extract_exprt & | to_byte_extract_expr (exprt &expr) |
void | validate_expr (const byte_extract_exprt &value) |
template<> | |
bool | can_cast_expr< byte_update_exprt > (const exprt &base) |
const byte_update_exprt & | to_byte_update_expr (const exprt &expr) |
byte_update_exprt & | to_byte_update_expr (exprt &expr) |
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. More... | |
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. More... | |
bool | has_byte_operator (const exprt &src) |
Return true iff src or one of its operands contain a byte extract or byte update expression. More... | |
exprt | lower_byte_extract (const byte_extract_exprt &src, const namespacet &ns) |
Rewrite a byte extract expression to more fundamental operations. More... | |
exprt | lower_byte_update (const byte_update_exprt &src, const namespacet &ns) |
Rewrite a byte update expression to more fundamental operations. More... | |
exprt | lower_byte_operators (const exprt &src, const namespacet &ns) |
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations. More... | |
Expression classes for byte-level operators.
Definition in file byte_operators.h.
|
inline |
Definition at line 64 of file byte_operators.h.
|
inline |
Definition at line 137 of file byte_operators.h.
bool has_byte_operator | ( | const exprt & | src | ) |
Return true iff src
or one of its operands contain a byte extract or byte update expression.
Definition at line 61 of file byte_operators.cpp.
exprt lower_byte_extract | ( | const byte_extract_exprt & | src, |
const namespacet & | ns | ||
) |
Rewrite a byte extract expression to more fundamental operations.
src | Byte extract expression |
ns | Namespace |
src
.Rewrite a byte extract expression to more fundamental operations.
Definition at line 1215 of file lower_byte_operators.cpp.
exprt lower_byte_operators | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.
src | Input expression |
ns | Namespace |
Definition at line 2640 of file lower_byte_operators.cpp.
exprt lower_byte_update | ( | const byte_update_exprt & | src, |
const namespacet & | ns | ||
) |
Rewrite a byte update expression to more fundamental operations.
src | Byte update expression |
ns | Namespace |
src
. Definition at line 2547 of file lower_byte_operators.cpp.
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.
Definition at line 48 of file byte_operators.cpp.
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.
Definition at line 55 of file byte_operators.cpp.
|
inline |
Definition at line 70 of file byte_operators.h.
|
inline |
Definition at line 76 of file byte_operators.h.
|
inline |
Definition at line 143 of file byte_operators.h.
|
inline |
Definition at line 149 of file byte_operators.h.
|
inline |
Definition at line 82 of file byte_operators.h.