cprover
cone_of_influence.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_CONE_OF_INFLUENCE_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_CONE_OF_INFLUENCE_H
14 
16 
17 #include <util/std_expr.h>
18 #include <util/ref_expr_set.h>
19 #include <util/symbol_table.h>
20 
21 typedef std::unordered_set<exprt, irep_hash> expr_sett;
22 
23 void cone_of_influence(goto_programt &program,
24  expr_sett &targets,
25  expr_sett &cone);
26 
28 {
29  public:
31  const symbol_tablet &symbol_table) :
32  program(_program),
33  ns(symbol_table)
34  {
35  }
36 
37  void cone_of_influence(const expr_sett &targets, expr_sett &cone);
38  void cone_of_influence(const exprt &target, expr_sett &cone);
39 
40  protected:
42  const expr_sett &curr,
43  expr_sett &next);
44  void get_succs(goto_programt::instructionst::const_reverse_iterator rit,
45  expr_sett &targets);
46  void gather_rvalues(const exprt &expr, expr_sett &rvals);
47 
48  typedef std::unordered_map<unsigned int, expr_sett> cone_mapt;
50 
52  const namespacet ns;
53 };
54 
55 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_CONE_OF_INFLUENCE_H
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
Value Set.
const goto_programt & program
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
std::unordered_set< exprt, irep_hash > expr_sett
std::unordered_map< unsigned int, expr_sett > cone_mapt
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void gather_rvalues(const exprt &expr, expr_sett &rvals)
cone_of_influencet(const goto_programt &_program, const symbol_tablet &symbol_table)
void cone_of_influence(goto_programt &program, expr_sett &targets, expr_sett &cone)
Base class for all expressions.
Definition: expr.h:42
const namespacet ns
Concrete Goto Program.