cprover
value_set_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
14 
15 #define USE_DEPRECATED_STATIC_ANALYSIS_H
17 
18 #include "value_set_domain.h"
19 #include "value_sets.h"
20 
21 class xmlt;
22 
24  const std::function<const value_sett &(goto_programt::const_targett)>
25  &get_value_set,
26  const goto_programt &goto_program,
27  xmlt &dest);
28 
36 template<class VSDT>
38  public value_setst,
39  public static_analysist<VSDT>
40 {
41 public:
42  typedef VSDT domaint;
44  typedef typename baset::locationt locationt;
45 
47  {
48  }
49 
51  {
52  return (*this)[t].value_set;
53  }
54 
55  void convert(
56  const goto_programt &goto_program,
57  xmlt &dest) const
58  {
59  using std::placeholders::_1;
61  std::bind(&value_set_analysis_templatet::get_value_set, *this, _1),
62  goto_program,
63  dest);
64  }
65 
66 public:
67  // interface value_sets
68  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
69  void get_values(
70  const irep_idt &,
71  locationt l,
72  const exprt &expr,
73  value_setst::valuest &dest) override
74  {
75  (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
76  }
77 
78  // interface value_sets
79  std::vector<exprt>
80  get_values(const irep_idt &, locationt l, const exprt &expr) override
81  {
82  return (*this)[l].value_set.get_value_set(expr, baset::ns);
83  }
84 };
85 
86 typedef
89 
90 void convert(
91  const goto_functionst &goto_functions,
92  const value_set_analysist &value_set_analysis,
93  xmlt &dest);
94 
95 void convert(
96  const goto_programt &goto_program,
97  const value_set_analysist &value_set_analysis,
98  xmlt &dest);
99 
100 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
value_set_domain.h
Value Set.
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_analysis_templatet::convert
void convert(const goto_programt &goto_program, xmlt &dest) const
Definition: value_set_analysis.h:55
value_set_analysis_templatet::domaint
VSDT domaint
Definition: value_set_analysis.h:42
value_set_analysis_templatet
This template class implements a data-flow analysis which keeps track of what values different variab...
Definition: value_set_analysis.h:40
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
exprt
Base class for all expressions.
Definition: expr.h:53
static_analysis.h
Static Analysis.
value_set_analysist
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
Definition: value_set_analysis.h:88
value_sets.h
Value Set Propagation.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_sets_to_xml
void value_sets_to_xml(const std::function< const value_sett &(goto_programt::const_targett)> &get_value_set, const goto_programt &goto_program, xmlt &dest)
Definition: value_set_analysis.cpp:20
value_set_analysis_templatet::baset
static_analysist< domaint > baset
Definition: value_set_analysis.h:43
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
static_analysist::locationt
goto_programt::const_targett locationt
Definition: static_analysis.h:288
static_analysist
Definition: static_analysis.h:280
value_set_analysis_templatet::locationt
baset::locationt locationt
Definition: value_set_analysis.h:44
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
xmlt
Definition: xml.h:21
static_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: static_analysis.h:103
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
value_setst
Definition: value_sets.h:22
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
value_set_analysis_templatet::value_set_analysis_templatet
value_set_analysis_templatet(const namespacet &ns)
Definition: value_set_analysis.h:46
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
value_set_analysis_templatet::get_values
void get_values(const irep_idt &, locationt l, const exprt &expr, value_setst::valuest &dest) override
Definition: value_set_analysis.h:69
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
convert
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
Definition: value_set_analysis.cpp:72
value_set_analysis_templatet::get_value_set
const value_sett & get_value_set(goto_programt::const_targett t)
Definition: value_set_analysis.h:50
value_set_analysis_templatet::get_values
std::vector< exprt > get_values(const irep_idt &, locationt l, const exprt &expr) override
Definition: value_set_analysis.h:80
static_analysis_baset::ns
const namespacet & ns
Definition: static_analysis.h:178