cprover
byte_operators.cpp File Reference
+ Include dependency graph for 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 lower_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...
 
static exprt lower_byte_update (const byte_update_exprt &src, const namespacet &ns, bool negative_offset)
 
static exprt lower_byte_update (const byte_update_exprt &src, const namespacet &ns)
 
bool has_byte_operator (const exprt &src)
 
exprt lower_byte_operators (const exprt &src, const namespacet &ns)
 

Function Documentation

◆ has_byte_operator()

bool has_byte_operator ( const exprt src)

Definition at line 630 of file byte_operators.cpp.

◆ lower_byte_extract()

exprt lower_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 166 of file byte_operators.cpp.

◆ lower_byte_operators()

exprt lower_byte_operators ( const exprt src,
const namespacet ns 
)

Definition at line 645 of file byte_operators.cpp.

◆ lower_byte_update() [1/2]

static exprt lower_byte_update ( const byte_update_exprt src,
const namespacet ns 
)
static

Definition at line 623 of file byte_operators.cpp.

◆ lower_byte_update() [2/2]

static exprt lower_byte_update ( const byte_update_exprt src,
const namespacet ns,
bool  negative_offset 
)
static

Definition at line 358 of file byte_operators.cpp.

◆ 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
Exceptions
flatten_byte_extract_exceptiontRaised is unable to unpack the object because of either non constant size, byte misalignment or non-constant component width.

Definition at line 32 of file byte_operators.cpp.