CBMC
propagate.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Propagate
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPROVER_PROPAGATE_H
13 #define CPROVER_CPROVER_PROPAGATE_H
14 
15 #include "solver_types.h"
16 
17 #include <unordered_set>
18 
19 void propagate(
20  const std::vector<framet> &,
21  const workt &,
22  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
23  bool verbose,
24  const namespacet &,
25  const std::function<void(const symbol_exprt &, exprt, const workt::patht &)>
26  &propagator);
27 
28 exprt simplify_state_expr(
29  exprt,
30  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
31  const namespacet &);
32 
33 exprt simplify_state_expr_node(
34  exprt,
35  const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
36  const namespacet &);
37 
38 #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
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131
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:961
propagate
void propagate(const std::vector< framet > &, const workt &, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &, const std::function< void(const symbol_exprt &, exprt, const workt::patht &)> &propagator)
Definition: propagate.cpp:24
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:1087
solver_types.h
Solver.
workt::patht
std::vector< frame_reft > patht
Definition: solver_types.h:167