cprover
Loading...
Searching...
No Matches
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 {
44 value_set.location_number=l->location_number;
45 }
46
47 void transform(
48 const namespacet &ns,
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 &,
70 const irep_idt &function_to,
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
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:40
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
Static Analysis.
Value Set.
value_set_domain_templatet< value_sett > value_set_domaint