cprover
global_may_alias.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive, over-approximative
4  escape analysis
5 
6 Author: Daniel Kroening, kroening@kroening.com
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
14 #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
15 
16 #include <util/numbering.h>
17 #include <util/threeval.h>
18 #include <util/union_find.h>
19 
20 #include "ai.h"
21 
23 
25 {
26 public:
28  {
29  }
30 
31  void transform(
32  locationt from,
33  locationt to,
34  ai_baset &ai,
35  const namespacet &ns) final;
36 
37  void output(
38  std::ostream &out,
39  const ai_baset &ai,
40  const namespacet &ns) const final;
41 
42  bool merge(
43  const global_may_alias_domaint &b,
44  locationt from,
45  locationt to);
46 
47  void make_bottom() final
48  {
49  aliases.clear();
50  has_values=tvt(false);
51  }
52 
53  void make_top() final
54  {
55  aliases.clear();
56  has_values=tvt(true);
57  }
58 
59  void make_entry() final
60  {
61  make_top();
62  }
63 
65  aliasest aliases;
66 
67 private:
69 
70  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
71  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
72  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
73 };
74 
75 class global_may_alias_analysist:public ait<global_may_alias_domaint>
76 {
77 protected:
78  virtual void initialize(const goto_functionst &_goto_functions)
79  {
80  }
81 };
82 
83 #endif // CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
virtual void initialize(const goto_functionst &_goto_functions)
bool merge(const global_may_alias_domaint &b, locationt from, locationt to)
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Definition: ai.h:342
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void clear()
Definition: union_find.h:238
Abstract Interpretation.
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
goto_programt::const_targett locationt
Definition: ai.h:42
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
union_find< irep_idt > aliasest