cprover
value_set_domain_fivrns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Domain (Flow Insensitive, 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_FIVRNS_H
14 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVRNS_H
15 
17 
18 #include "value_set_fivrns.h"
19 
22 {
23 public:
25 
26  // overloading
27 
28  virtual void output(
29  const namespacet &ns,
30  std::ostream &out) const
31  {
32  value_set.output(ns, out);
33  }
34 
35  virtual void initialize(
36  const namespacet &)
37  {
38  value_set.clear();
39  }
40 
41  virtual bool transform(
42  const namespacet &ns,
43  const irep_idt &function_from,
44  locationt from_l,
45  const irep_idt &function_to,
46  locationt to_l);
47 
48  virtual void get_reference_set(
49  const namespacet &ns,
50  const exprt &expr,
51  expr_sett &expr_set)
52  {
53  value_set.get_reference_set(expr, expr_set, ns);
54  }
55 
56  virtual void clear(void)
57  {
58  value_set.clear();
59  }
60 };
61 
62 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVRNS_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_fivrnst::value_set
value_set_fivrnst value_set
Definition: value_set_domain_fivrns.h:24
value_set_fivrnst::output
void output(const namespacet &ns, std::ostream &out) const
exprt
Base class for all expressions.
Definition: expr.h:53
value_set_fivrns.h
Value Set (Flow Insensitive, Validity Regions)
value_set_domain_fivrnst::clear
virtual void clear(void)
Definition: value_set_domain_fivrns.h:56
value_set_fivrnst
Definition: value_set_fivrns.h:31
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:44
value_set_domain_fivrnst::output
virtual void output(const namespacet &ns, std::ostream &out) const
Definition: value_set_domain_fivrns.h:28
value_set_fivrnst::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
flow_insensitive_abstract_domain_baset::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: flow_insensitive_analysis.h:65
value_set_domain_fivrnst::transform
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l)
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
value_set_domain_fivrnst::get_reference_set
virtual void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)
Definition: value_set_domain_fivrns.h:48
value_set_fivrnst::clear
void clear()
Definition: value_set_fivrns.h:239
flow_insensitive_abstract_domain_baset
Definition: flow_insensitive_analysis.h:37
value_set_domain_fivrnst::initialize
virtual void initialize(const namespacet &)
Definition: value_set_domain_fivrns.h:35
value_set_domain_fivrnst
Definition: value_set_domain_fivrns.h:22