cprover
expr_lowering.h File Reference
#include <util/expr.h>
+ Include dependency graph for expr_lowering.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

exprt lower_byte_extract (const byte_extract_exprt &src, const namespacet &ns)
 Rewrite a byte extract expression to more fundamental operations. More...
 
exprt lower_byte_update (const byte_update_exprt &src, const namespacet &ns)
 Rewrite a byte update expression to more fundamental operations. More...
 
exprt lower_byte_operators (const exprt &src, const namespacet &ns)
 Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations. More...
 
bool has_byte_operator (const exprt &src)
 
exprt lower_popcount (const popcount_exprt &expr, const namespacet &ns)
 Lower a popcount_exprt to arithmetic and logic expressions. More...
 

Function Documentation

◆ has_byte_operator()

bool has_byte_operator ( const exprt src)

Definition at line 2302 of file byte_operators.cpp.

◆ lower_byte_extract()

exprt lower_byte_extract ( const byte_extract_exprt src,
const namespacet ns 
)

Rewrite a byte extract expression to more fundamental operations.

Parameters
srcByte extract expression
nsNamespace
Returns
Semantically equivalent expression such that the top-level expression no longer is a byte_extract_exprt or byte_update_exprt. Use lower_byte_operators to also remove all byte operators from any operands of src.

Rewrite a byte extract expression to more fundamental operations.

Definition at line 999 of file byte_operators.cpp.

◆ lower_byte_operators()

exprt lower_byte_operators ( const exprt src,
const namespacet ns 
)

Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.

Parameters
srcInput expression
nsNamespace
Returns
Semantically equivalent expression that does not contain any byte_extract_exprt or byte_update_exprt.

Definition at line 2317 of file byte_operators.cpp.

◆ lower_byte_update()

exprt lower_byte_update ( const byte_update_exprt src,
const namespacet ns 
)

Rewrite a byte update expression to more fundamental operations.

Parameters
srcByte update expression
nsNamespace
Returns
Semantically equivalent expression such that the top-level expression no longer is a byte_extract_exprt or byte_update_exprt. Use lower_byte_operators to also remove all byte operators from any operands of src.

Definition at line 2256 of file byte_operators.cpp.

◆ lower_popcount()

exprt lower_popcount ( const popcount_exprt expr,
const namespacet ns 
)

Lower a popcount_exprt to arithmetic and logic expressions.

Parameters
exprInput expression to be translated
nsNamespace for type lookups
Returns
Semantically equivalent expression

Definition at line 16 of file popcount.cpp.