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 
20 template<class VST>
22 {
23 public:
24  VST value_set;
25 
26  // overloading
27 
29  {
30  return value_set.make_union(other.value_set);
31  }
32 
33  virtual void output(
34  const namespacet &ns,
35  std::ostream &out) const
36  {
37  value_set.output(ns, out);
38  }
39 
40  virtual void initialize(
41  const namespacet &,
42  locationt l)
43  {
44  value_set.clear();
45  value_set.location_number=l->location_number;
46  }
47 
48  virtual void transform(
49  const namespacet &ns,
50  const irep_idt &function_from,
51  locationt from_l,
52  const irep_idt &function_to,
53  locationt to_l);
54 
55  virtual void get_reference_set(
56  const namespacet &ns,
57  const exprt &expr,
59  {
60  value_set.get_reference_set(expr, dest, ns);
61  }
62 };
63 
65 
66 #include "value_set_domain_transform.inc"
67 
68 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H
virtual void output(const namespacet &ns, std::ostream &out) const
Value Set.
goto_programt::const_targett locationt
virtual void initialize(const namespacet &, locationt l)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Static Analysis.
virtual void get_reference_set(const namespacet &ns, const exprt &expr, value_setst::valuest &dest)
virtual void transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l)
Base class for all expressions.
Definition: expr.h:54
std::list< exprt > valuest
Definition: value_sets.h:28
bool merge(const value_set_domain_templatet< VST > &other, locationt)
value_set_domain_templatet< value_sett > value_set_domaint