cprover
value_set_domain.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set
4
5Author: 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
23template<class VST>
25{
26public:
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
65template <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:
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:
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