cprover
function_modifies.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Modifies
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
13 #define CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
14 
16 
17 #include <map>
18 
19 class goto_functionst;
20 class local_may_aliast;
21 
23 {
24 public:
25  explicit function_modifiest(const goto_functionst &_goto_functions):
26  goto_functions(_goto_functions)
27  {
28  }
29 
30  typedef std::set<exprt> modifiest;
31 
32  void get_modifies(
33  const local_may_aliast &local_may_alias,
35  modifiest &);
36 
38  const exprt &,
39  modifiest &);
40 
41  void operator()(const exprt &function, modifiest &modifies)
42  {
43  get_modifies_function(function, modifies);
44  }
45 
46 protected:
48 
49  typedef std::map<irep_idt, modifiest> function_mapt;
51 };
52 
53 #endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
function_modifiest
Definition: function_modifies.h:23
function_modifiest::operator()
void operator()(const exprt &function, modifiest &modifies)
Definition: function_modifies.h:41
function_modifiest::function_map
function_mapt function_map
Definition: function_modifies.h:50
exprt
Base class for all expressions.
Definition: expr.h:54
function_modifiest::goto_functions
const goto_functionst & goto_functions
Definition: function_modifies.h:47
local_may_aliast
Definition: local_may_alias.h:26
function_modifiest::function_modifiest
function_modifiest(const goto_functionst &_goto_functions)
Definition: function_modifies.h:25
goto_program.h
Concrete Goto Program.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
function_modifiest::get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
Definition: function_modifies.cpp:20
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
function_modifiest::function_mapt
std::map< irep_idt, modifiest > function_mapt
Definition: function_modifies.h:49
function_modifiest::modifiest
std::set< exprt > modifiest
Definition: function_modifies.h:30
function_modifiest::get_modifies_function
void get_modifies_function(const exprt &, modifiest &)
Definition: function_modifies.cpp:44