CBMC
simplify_state_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Simplify State Expression
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPROVER_SIMPLIFY_STATE_EXPR_H
13 #define CPROVER_CPROVER_SIMPLIFY_STATE_EXPR_H
14 
15 #include <util/std_expr.h> // IWYU pragma: keep
16 
17 #include <unordered_set>
18 
19 class namespacet;
20 
21 exprt simplify_state_expr(
22  exprt,
23  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
24  const namespacet &);
25 
26 exprt simplify_state_expr_node(
27  exprt,
28  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
29  const namespacet &);
30 
31 #endif // CPROVER_CPROVER_PROPAGATE_H
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition: address_taken.cpp:51
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
simplify_state_expr_node
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition: simplify_state_expr.cpp:957
simplify_state_expr
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition: simplify_state_expr.cpp:1083
std_expr.h
API to expression classes.