cprover
ai_domain.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_AI_DOMAIN_H
13 #define CPROVER_ANALYSES_AI_DOMAIN_H
14 
15 #include <util/expr.h>
16 #include <util/json.h>
17 #include <util/make_unique.h>
18 #include <util/xml.h>
19 
21 
22 // forward reference the abstract interpreter interface
23 class ai_baset;
24 
28 {
29 protected:
32  {
33  }
34 
35 public:
36  virtual ~ai_domain_baset()
37  {
38  }
39 
41 
56 
57  virtual void transform(
58  locationt from,
59  locationt to,
60  ai_baset &ai,
61  const namespacet &ns) = 0;
62 
63  virtual void
64  output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
65  {
66  }
67 
68  virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
69 
70  virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
71 
73  virtual void make_bottom() = 0;
74 
77  virtual void make_top() = 0;
78 
80  virtual void make_entry() = 0;
81 
82  virtual bool is_bottom() const = 0;
83 
84  virtual bool is_top() const = 0;
85 
97 
101 
103  virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
104  {
105  return true;
106  }
107 
109  virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
110 
113  virtual exprt to_predicate(void) const
114  {
115  if(is_bottom())
116  return false_exprt();
117  else
118  return true_exprt();
119  }
120 };
121 
122 #endif
virtual bool is_top() const =0
virtual void make_bottom()=0
no states
Definition: json.h:23
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:16
virtual bool is_bottom() const =0
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Symbol Table + CFG.
The boolean constant true.
Definition: std_expr.h:4486
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
also add
Definition: ai_domain.h:103
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Definition: xml.h:18
virtual exprt to_predicate(void) const
Gives a Boolean condition that is true for all values represented by the domain.
Definition: ai_domain.h:113
The boolean constant false.
Definition: std_expr.h:4497
ai_domain_baset()
The constructor is expected to produce &#39;false&#39; or &#39;bottom&#39;.
Definition: ai_domain.h:31
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Simplifies the expression but keeps it as an l-value.
Definition: ai_domain.cpp:42
The basic interface of an abstract interpreter.
Definition: ai.h:32
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:25
Base class for all expressions.
Definition: expr.h:42
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.h:64
virtual ~ai_domain_baset()
Definition: ai_domain.h:36
goto_programt::const_targett locationt
Definition: ai_domain.h:40
virtual void make_top()=0
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it...
virtual void make_entry()=0
a reasonable entry-point state