CBMC
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
15#include <util/namespace.h>
16
18
19#include <unordered_set>
20
21typedef std::unordered_set<exprt, irep_hash> expr_sett;
22
24 expr_sett &targets,
26
28{
29public:
32 const symbol_table_baset &symbol_table)
33 : program(_program), 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
40protected:
43 const expr_sett &curr,
44 expr_sett &next);
45 void get_succs(
46 goto_programt::instructionst::const_reverse_iterator rit,
47 expr_sett &targets);
48 void gather_rvalues(const exprt &expr, expr_sett &rvals);
49
50 typedef std::unordered_map<unsigned int, expr_sett> cone_mapt;
52
55};
56
57#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_CONE_OF_INFLUENCE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const goto_programt & program
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
cone_of_influencet(const goto_programt &_program, const symbol_table_baset &symbol_table)
const namespacet ns
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
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:56
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 base class interface.
void cone_of_influence(goto_programt &program, expr_sett &targets, expr_sett &cone)
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.