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 
17 
19 {
20 public:
21  explicit function_modifiest(const goto_functionst &_goto_functions):
22  goto_functions(_goto_functions)
23  {
24  }
25 
26  typedef std::set<exprt> modifiest;
27 
28  void get_modifies(
29  const local_may_aliast &local_may_alias,
31  modifiest &);
32 
33  void get_modifies_lhs(
34  const local_may_aliast &,
36  const exprt &lhs,
37  modifiest &);
38 
40  const exprt &,
41  modifiest &);
42 
43  void operator()(const exprt &function, modifiest &modifies)
44  {
45  get_modifies_function(function, modifies);
46  }
47 
48 protected:
50 
51  typedef std::map<irep_idt, modifiest> function_mapt;
53 };
54 
55 #endif // CPROVER_GOTO_INSTRUMENT_FUNCTION_MODIFIES_H
std::set< exprt > modifiest
function_modifiest(const goto_functionst &_goto_functions)
Goto Programs with Functions.
std::map< irep_idt, modifiest > function_mapt
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
void operator()(const exprt &function, modifiest &modifies)
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A collection of goto functions.
Base class for all expressions.
Definition: expr.h:54
const goto_functionst & goto_functions
function_mapt function_map
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
void get_modifies_function(const exprt &, modifiest &)
Field-insensitive, location-sensitive may-alias analysis.