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 &ns, std::ostream &out) const override
37  {
38  value_set.output(ns, 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 RETURN:
87  case OTHER:
88  case ASSIGN:
89  case DECL:
90  case DEAD:
91  value_set.apply_code(from_l->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  {
100  const code_function_callt &code = to_code_function_call(from_l->code);
101 
102  value_set.do_function_call(function_to, code.arguments(), ns);
103  }
104  break;
105 
106  case ASSERT:
107  case SKIP:
108  case START_THREAD:
109  case END_THREAD:
110  case LOCATION:
111  case ATOMIC_BEGIN:
112  case ATOMIC_END:
113  case THROW:
114  case CATCH:
115  case INCOMPLETE_GOTO:
116  case NO_INSTRUCTION_TYPE:
117  {
118  // do nothing
119  }
120  }
121 }
122 
123 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
value_set_domain_templatet
This is the domain for a value set analysis.
Definition: value_set_domain.h:25
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_set_domain_templatet::output
void output(const namespacet &ns, std::ostream &out) const override
Definition: value_set_domain.h:36
domain_baset
Definition: static_analysis.h:31
value_set_domaint
value_set_domain_templatet< value_sett > value_set_domaint
Definition: value_set_domain.h:63
exprt
Base class for all expressions.
Definition: expr.h:53
value_set_domain_templatet::transform
void transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
Definition: value_set_domain.h:66
static_analysis_baset::get_return_lhs
static exprt get_return_lhs(locationt to)
Definition: static_analysis.cpp:36
static_analysis.h
Static Analysis.
value_set_domain_templatet::get_reference_set
void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest) override
Definition: value_set_domain.h:54
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:50
domain_baset::locationt
goto_programt::const_targett locationt
Definition: static_analysis.h:41
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
value_set.h
Value Set.
GOTO
@ GOTO
Definition: goto_program.h:34
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
value_set_domain_templatet::initialize
void initialize(const namespacet &, locationt l) override
Definition: value_set_domain.h:41
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
OTHER
@ OTHER
Definition: goto_program.h:37
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
RETURN
@ RETURN
Definition: goto_program.h:45
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
CATCH
@ CATCH
Definition: goto_program.h:51
value_set_domain_templatet::merge
bool merge(const value_set_domain_templatet< VST > &other, locationt)
Definition: value_set_domain.h:31
DECL
@ DECL
Definition: goto_program.h:47
ASSUME
@ ASSUME
Definition: goto_program.h:35
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
DEAD
@ DEAD
Definition: goto_program.h:48
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
LOCATION
@ LOCATION
Definition: goto_program.h:41
ASSERT
@ ASSERT
Definition: goto_program.h:36
value_set_domain_templatet::value_set
VST value_set
Definition: value_set_domain.h:27
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52