cprover
value_set_domain_fivr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set (Flow Insensitive, Sharing, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_H
14 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_H
15 
17 
18 #include "value_set_fivr.h"
19 
21 {
22 public:
24 
25  // overloading
26 
27  void output(const namespacet &ns, std::ostream &out) const override
28  {
29  value_set.output(ns, out);
30  }
31 
32  void initialize(const namespacet &) override
33  {
34  value_set.clear();
35  }
36 
37  bool transform(
38  const namespacet &ns,
39  const irep_idt &function_from,
40  locationt from_l,
41  const irep_idt &function_to,
42  locationt to_l) override;
43 
45  const namespacet &ns,
46  const exprt &expr,
47  expr_sett &expr_set) override
48  {
49  value_set.get_reference_set(expr, expr_set, ns);
50  }
51 
52  void clear(void) override
53  {
54  value_set.clear();
55  }
56 };
57 
58 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_H
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_fivrt::clear
void clear(void) override
Definition: value_set_domain_fivr.h:52
value_set_fivrt::output
void output(const namespacet &ns, std::ostream &out) const
value_set_domain_fivrt::initialize
void initialize(const namespacet &) override
Definition: value_set_domain_fivr.h:32
exprt
Base class for all expressions.
Definition: expr.h:53
value_set_fivrt
Definition: value_set_fivr.h:30
value_set_fivrt::clear
void clear()
Definition: value_set_fivr.h:247
value_set_domain_fivrt::get_reference_set
void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set) override
Definition: value_set_domain_fivr.h:44
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_domain_fivrt::output
void output(const namespacet &ns, std::ostream &out) const override
Definition: value_set_domain_fivr.h:27
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:44
value_set_domain_fivrt::value_set
value_set_fivrt value_set
Definition: value_set_domain_fivr.h:23
value_set_domain_fivrt::transform
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
flow_insensitive_abstract_domain_baset::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: flow_insensitive_analysis.h:65
value_set_domain_fivrt
Definition: value_set_domain_fivr.h:21
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
flow_insensitive_abstract_domain_baset
Definition: flow_insensitive_analysis.h:37
value_set_fivr.h
Value Set (Flow Insensitive, Sharing, Validity Regions)
value_set_fivrt::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const