cprover
flatten_byte_operators.h File Reference
This graph shows which files directly or indirectly include this file:

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)
 

Function Documentation

§ flatten_byte_extract()

§ flatten_byte_operators()

§ flatten_byte_update()

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)