cprover
value_set_domain.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
14 
15 #define USE_DEPRECATED_STATIC_ANALYSIS_H
17 
18 #include "value_set.h"
19 
23 template<class VST>
25 {
26 public:
27  VST value_set;
28 
29  // overloading
30 
32  {
33  return value_set.make_union(other.value_set);
34  }
35 
36  void output(const namespacet &, std::ostream &out) const override
37  {
38  value_set.output(out);
39  }
40 
41  void initialize(const namespacet &, locationt l) override
42  {
43  value_set.clear();
44  value_set.location_number=l->location_number;
45  }
46 
47  void transform(
48  const namespacet &ns,
49  const irep_idt &function_from,
50  locationt from_l,
51  const irep_idt &function_to,
52  locationt to_l) override;
53 
55  const namespacet &ns,
56  const exprt &expr,
57  value_setst::valuest &dest) override
58  {
59  value_set.get_reference_set(expr, dest, ns);
60  }
61 };
62 
64 
65 template <class VST>
67  const namespacet &ns,
68  const irep_idt &,
69  locationt from_l,
70  const irep_idt &function_to,
71  locationt to_l)
72 {
73  switch(from_l->type())
74  {
75  case GOTO:
76  // ignore for now
77  break;
78 
79  case END_FUNCTION:
80  {
81  value_set.do_end_function(static_analysis_baset::get_return_lhs(to_l), ns);
82  break;
83  }
84 
85  // Note intentional fall-through here:
86  case SET_RETURN_VALUE:
87  case OTHER:
88  case ASSIGN:
89  case DECL:
90  case DEAD:
91  value_set.apply_code(from_l->get_code(), ns);
92  break;
93 
94  case ASSUME:
95  value_set.guard(from_l->get_condition(), ns);
96  break;
97 
98  case FUNCTION_CALL:
99  value_set.do_function_call(function_to, from_l->call_arguments(), ns);
100  break;
101 
102  case ASSERT:
103  case SKIP:
104  case START_THREAD:
105  case END_THREAD:
106  case LOCATION:
107  case ATOMIC_BEGIN:
108  case ATOMIC_END:
109  case THROW:
110  case CATCH:
111  case INCOMPLETE_GOTO:
112  case NO_INSTRUCTION_TYPE:
113  {
114  // do nothing
115  }
116  }
117 }
118 
119 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
goto_programt::const_targett locationt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
static exprt get_return_lhs(locationt to)
This is the domain for a value set analysis.
void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest) override
void initialize(const namespacet &, locationt l) override
void output(const namespacet &, std::ostream &out) const override
void transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
bool merge(const value_set_domain_templatet< VST > &other, locationt)
std::list< exprt > valuest
Definition: value_sets.h:28
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
Static Analysis.
Value Set.
value_set_domain_templatet< value_sett > value_set_domaint