cprover
|
#include "flatten_byte_operators.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/replace_symbol.h>
#include <util/simplify_expr.h>
#include "flatten_byte_extract_exceptions.h"
Go to the source code of this file.
Functions | |
static exprt | unpack_rec (const exprt &src, bool little_endian, const exprt &max_bytes, const namespacet &ns, bool unpack_byte_array=false) |
rewrite an object into its individual bytes More... | |
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, bool negative_offset) |
exprt | flatten_byte_update (const byte_update_exprt &src, const namespacet &ns) |
bool | has_byte_operator (const exprt &src) |
exprt | flatten_byte_operators (const exprt &src, const namespacet &ns) |
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 153 of file flatten_byte_operators.cpp.
References struct_union_typet::components(), exprt::copy_to_operands(), DATA_INVARIANT, 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(), simplify_expr(), array_typet::size(), size_of_expr(), typet::subtype(), to_array_type(), to_integer(), to_struct_type(), exprt::type(), unpack_rec(), and UNREACHABLE.
Referenced by 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 621 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, | ||
bool | negative_offset | ||
) |
Definition at line 347 of file flatten_byte_operators.cpp.
References flatten_byte_extract(), namespace_baset::follow(), from_integer(), irept::id(), irept::id_string(), integer2size_t(), integer2unsigned(), exprt::make_typecast(), byte_extract_exprt::op(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_offset_bits(), pointer_offset_size(), power(), irept::pretty(), simplify_expr(), typet::subtype(), irept::swap(), to_array_type(), and exprt::type().
Referenced by flatten_byte_operators(), and flatten_byte_update().
exprt flatten_byte_update | ( | const byte_update_exprt & | src, |
const namespacet & | ns | ||
) |
Definition at line 599 of file flatten_byte_operators.cpp.
References flatten_byte_update().
bool has_byte_operator | ( | const exprt & | src | ) |
Definition at line 606 of file flatten_byte_operators.cpp.
References forall_operands, has_byte_operator(), and irept::id().
Referenced by boolbvt::convert_equality(), and has_byte_operator().
|
static |
rewrite an object into its individual bytes
flatten_byte_extract_exceptiont | Raised is unable to unpack the object because of either non constant size, byte misalignment or non-constant component width. |
Definition at line 30 of file flatten_byte_operators.cpp.
References struct_union_typet::components(), exprt::copy_to_operands(), namespace_baset::follow(), from_integer(), irept::id(), index_type(), replace_symbolt::insert(), exprt::operands(), pointer_offset_bits(), irept::pretty(), simplify(), array_typet::size(), size_type(), typet::subtype(), to_array_type(), to_integer(), to_struct_type(), and exprt::type().
Referenced by flatten_byte_extract().