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 
21 {
22 public:
24 
25  // overloading
26 
27  bool merge(const value_set_domaint &other, locationt to)
28  {
29  return value_set.make_union(other.value_set);
30  }
31 
32  virtual void output(
33  const namespacet &ns,
34  std::ostream &out) const
35  {
36  value_set.output(ns, out);
37  }
38 
39  virtual void initialize(
40  const namespacet &ns,
41  locationt l)
42  {
43  value_set.clear();
44  value_set.location_number=l->location_number;
45  }
46 
47  virtual void transform(
48  const namespacet &ns,
49  locationt from_l,
50  locationt to_l);
51 
52  virtual void get_reference_set(
53  const namespacet &ns,
54  const exprt &expr,
56  {
57  value_set.get_reference_set(expr, dest, ns);
58  }
59 };
60 
61 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set.cpp:246
virtual void output(const namespacet &ns, std::ostream &out) const
Value Set.
goto_programt::const_targett locationt
bool merge(const value_set_domaint &other, locationt to)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest)
Static Analysis.
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:909
Base class for all expressions.
Definition: expr.h:46
virtual void transform(const namespacet &ns, locationt from_l, locationt to_l)
void clear()
Definition: value_set.h:143
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set.cpp:97
virtual void initialize(const namespacet &ns, locationt l)
std::list< exprt > valuest
Definition: value_sets.h:28
unsigned location_number
Definition: value_set.h:37