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
32  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
33  final override;
34 
35  void output(
36  std::ostream &out,
37  const ai_baset &ai,
38  const namespacet &ns) const final override;
39 
40  bool merge(
41  const global_may_alias_domaint &b,
42  locationt from,
43  locationt to);
44 
45  void make_bottom() final override
46  {
47  aliases.clear();
48  has_values=tvt(false);
49  }
50 
51  void make_top() final override
52  {
53  aliases.clear();
54  has_values=tvt(true);
55  }
56 
57  void make_entry() final override
58  {
59  make_top();
60  }
61 
62  bool is_bottom() const final override
63  {
65  "If the domain is bottom, there must be no aliases");
66  return has_values.is_false();
67  }
68 
69  bool is_top() const final override
70  {
72  "If the domain is top, there must be no aliases");
73  return has_values.is_true();
74  }
75 
78 
79 private:
81 
82  void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
83  void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
84  void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
85 };
86 
87 class global_may_alias_analysist:public ait<global_may_alias_domaint>
88 {
89 protected:
90  virtual void initialize(const goto_functionst &)
91  {
92  }
93 };
94 
95 #endif // CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
bool is_false() const
Definition: threeval.h:26
void make_entry() final override
a reasonable entry-point state
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 override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Definition: ai.h:294
size_t size() const
Definition: union_find.h:265
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
Definition: threeval.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_true() const
Definition: threeval.h:25
void clear()
Definition: union_find.h:244
void make_bottom() final override
no states
Abstract Interpretation.
bool is_bottom() const final override
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it.
bool is_top() const final override
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
virtual void initialize(const goto_functionst &)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
union_find< irep_idt > aliasest