cprover
|
Go to the source code of this file.
Functions | |
exprt | flatten_byte_extract (const byte_extract_exprt &src, const namespacet &ns) |
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressions More... | |
exprt | flatten_byte_update (const byte_update_exprt &src, const namespacet &ns) |
exprt | flatten_byte_operators (const exprt &src, const namespacet &ns) |
bool | has_byte_operator (const exprt &src) |
exprt flatten_byte_extract | ( | const byte_extract_exprt & | src, |
const namespacet & | ns | ||
) |
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressions
Definition at line 147 of file flatten_byte_operators.cpp.
References struct_union_typet::components(), exprt::copy_to_operands(), flatten_byte_extract(), namespace_baset::follow(), from_integer(), irept::id(), integer2unsigned(), irept::is_not_nil(), member_offset_expr(), exprt::move_to_operands(), byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::operands(), pointer_offset_bits(), irept::pretty(), simplify_expr(), array_typet::size(), size_of_expr(), typet::subtype(), to_array_type(), to_integer(), to_struct_type(), exprt::type(), and unpack_rec().
Referenced by smt1_convt::convert_byte_extract(), boolbvt::convert_byte_extract(), smt2_convt::convert_byte_extract(), flatten_byte_extract(), flatten_byte_operators(), and flatten_byte_update().
exprt flatten_byte_operators | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
Definition at line 616 of file flatten_byte_operators.cpp.
References flatten_byte_extract(), flatten_byte_operators(), flatten_byte_update(), Forall_operands, irept::id(), to_byte_extract_expr(), and to_byte_update_expr().
Referenced by boolbvt::convert_equality(), and flatten_byte_operators().
exprt flatten_byte_update | ( | const byte_update_exprt & | src, |
const namespacet & | ns | ||
) |
Definition at line 594 of file flatten_byte_operators.cpp.
References flatten_byte_update().
bool has_byte_operator | ( | const exprt & | src | ) |
Definition at line 601 of file flatten_byte_operators.cpp.
References forall_operands, has_byte_operator(), and irept::id().
Referenced by boolbvt::convert_equality(), and has_byte_operator().