cprover
Loading...
Searching...
No Matches
global_may_alias.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive, over-approximative
4 escape analysis
5
6Author: 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{
24public:
28
30 void transform(
31 const irep_idt &function_from,
32 trace_ptrt trace_from,
33 const irep_idt &function_to,
34 trace_ptrt trace_to,
35 ai_baset &ai,
36 const namespacet &ns) final override;
37
43 void output(
44 std::ostream &out,
45 const ai_baset &ai,
46 const namespacet &ns) const final override;
47
49 bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to);
50
52 void make_bottom() final override
53 {
54 aliases.clear();
55 has_values=tvt(false);
56 }
57
59 void make_top() final override
60 {
61 aliases.clear();
62 has_values=tvt(true);
63 }
64
66 bool is_bottom() const final override
67 {
68 DATA_INVARIANT(!has_values.is_false() || (aliases.size()==0),
69 "If the domain is bottom, there must be no aliases");
70 return has_values.is_false();
71 }
72
74 bool is_top() const final override
75 {
76 DATA_INVARIANT(!has_values.is_true() || (aliases.size()==0),
77 "If the domain is top, there must be no aliases");
78 return has_values.is_true();
79 }
80
83
84private:
86
87 void assign_lhs_aliases(const exprt &, const std::set<irep_idt> &);
88 void get_rhs_aliases(const exprt &, std::set<irep_idt> &);
89 void get_rhs_aliases_address_of(const exprt &, std::set<irep_idt> &);
90};
91
96class global_may_alias_analysist:public ait<global_may_alias_domaint>
97{
98protected:
99 virtual void initialize(const goto_functionst &)
100 {
101 }
102};
103
104#endif // CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the d...
Definition ai_domain.h:58
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:73
Base class for all expressions.
Definition expr.h:56
This is a may analysis (i.e.
virtual void initialize(const goto_functionst &)
Initialize all the abstract states for a whole program.
bool is_bottom() const final override
Returns true if domain is bottom.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Abstract Interpretation domain transform function.
union_find< irep_idt > aliasest
void make_bottom() final override
Clear list of aliases, and mark domain as bottom.
void make_top() final override
Clear list of aliases, and mark domain as top.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Abstract Interpretation domain output function.
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Specialisation of global_may_alias_domaint::get_rhs_aliases to deal with address_of expressions.
bool merge(const global_may_alias_domaint &b, trace_ptrt from, trace_ptrt to)
Abstract Interpretation domain merge function.
bool is_top() const final override
Returns false if domain is top.
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which is an object is being read.
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Populate list of aliases for a given identifier in a context in which an object is being written to.
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Definition threeval.h:20
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
dstringt irep_idt