cprover
flatten_byte_operators.cpp File Reference
Include dependency graph for flatten_byte_operators.cpp:

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)
 

Function Documentation

§ flatten_byte_extract()

§ flatten_byte_operators()

§ flatten_byte_update() [1/2]

§ flatten_byte_update() [2/2]

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().

§ has_byte_operator()

bool has_byte_operator ( const exprt src)

§ unpack_rec()

static exprt unpack_rec ( const exprt src,
bool  little_endian,
const exprt max_bytes,
const namespacet ns,
bool  unpack_byte_array = false 
)
static

rewrite an object into its individual bytes

parameters: src object to unpack
little_endian true, iff assumed endianness is little-endian max_bytes if not nil, use as upper bound of the number of bytes to unpack ns namespace for type lookups
Returns
array of bytes in the sequence found in memory

Definition at line 28 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().