cprover
Loading...
Searching...
No Matches
expr_lowering.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Lower expressions to arithmetic and logic expressions
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
10#define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
11
12#include <util/expr.h>
13
16class namespacet;
17
26
35
42exprt lower_byte_operators(const exprt &src, const namespacet &ns);
43
44bool has_byte_operator(const exprt &src);
45
46#endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
bool has_byte_operator(const exprt &src)
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...