|
CBMC
|
Include dependency graph for byte_operators.cpp:Go to the source code of this file.
Functions | |
| static irep_idt | byte_extract_id () |
| static irep_idt | byte_update_id () |
| 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. | |
| 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. | |
| 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 13 of file byte_operators.cpp.
Definition at line 30 of file byte_operators.cpp.
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.
| 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.