cprover
flatten_byte_operators.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H
11 #define CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H
12 
13 class byte_extract_exprt;
14 class byte_update_exprt;
15 class exprt;
16 class namespacet;
17 
19  const byte_extract_exprt &src,
20  const namespacet &ns);
21 
23  const byte_update_exprt &src,
24  const namespacet &ns);
25 
27  const exprt &src,
28  const namespacet &ns);
29 
30 bool has_byte_operator(const exprt &src);
31 
32 #endif // CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
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 expressi...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool has_byte_operator(const exprt &src)
Base class for all expressions.
Definition: expr.h:42
exprt flatten_byte_update(const byte_update_exprt &src, const namespacet &ns)
TO_BE_DOCUMENTED.
TO_BE_DOCUMENTED.