cprover
Loading...
Searching...
No Matches
cone_of_influence.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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/symbol_table.h>
18
19#include <unordered_set>
20
21typedef std::unordered_set<exprt, irep_hash> expr_sett;
22
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
53};
54
55#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_CONE_OF_INFLUENCE_H
const goto_programt & program
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
const namespacet ns
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
cone_of_influencet(const goto_programt &_program, const symbol_tablet &symbol_table)
void gather_rvalues(const exprt &expr, expr_sett &rvals)
std::unordered_map< unsigned int, expr_sett > cone_mapt
Base class for all expressions.
Definition expr.h:54
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table.
void cone_of_influence(goto_programt &program, expr_sett &targets, expr_sett &cone)
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
Author: Diffblue Ltd.