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 
29 template<class VSDT>
31  public value_setst,
32  public static_analysist<VSDT>
33 {
34 public:
35  typedef VSDT domaint;
37  typedef typename baset::locationt locationt;
38 
40  {
41  }
42 
44  {
45  return (*this)[t].value_set;
46  }
47 
48  void convert(
49  const goto_programt &goto_program,
50  xmlt &dest) const
51  {
52  using std::placeholders::_1;
54  std::bind(&value_set_analysis_templatet::get_value_set, *this, _1),
55  goto_program,
56  dest);
57  }
58 
59 public:
60  // interface value_sets
61  virtual void get_values(
62  locationt l,
63  const exprt &expr,
65  {
66  (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
67  }
68 };
69 
70 typedef
73 
74 void convert(
75  const goto_functionst &goto_functions,
76  const value_set_analysist &value_set_analysis,
77  xmlt &dest);
78 
79 void convert(
80  const goto_programt &goto_program,
81  const value_set_analysist &value_set_analysis,
82  xmlt &dest);
83 
84 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
value_set_domain.h
value_set_analysis_templatet::get_values
virtual void get_values(locationt l, const exprt &expr, value_setst::valuest &dest)
Definition: value_set_analysis.h:61
value_set_analysis_templatet::convert
void convert(const goto_programt &goto_program, xmlt &dest) const
Definition: value_set_analysis.h:48
value_set_analysis_templatet::domaint
VSDT domaint
Definition: value_set_analysis.h:35
value_set_analysis_templatet
Definition: value_set_analysis.h:30
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
exprt
Base class for all expressions.
Definition: expr.h:54
static_analysis.h
value_set_analysist
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
Definition: value_set_analysis.h:72
value_sets.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:21
value_set_analysis_templatet::baset
static_analysist< domaint > baset
Definition: value_set_analysis.h:36
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:279
value_set_analysis_templatet::locationt
baset::locationt locationt
Definition: value_set_analysis.h:37
xmlt
Definition: xml.h:18
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:22
value_setst
Definition: value_sets.h:21
value_set_analysis_templatet::value_set_analysis_templatet
value_set_analysis_templatet(const namespacet &ns)
Definition: value_set_analysis.h:39
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
convert
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
Definition: value_set_analysis.cpp:74
value_set_analysis_templatet::get_value_set
const value_sett & get_value_set(goto_programt::const_targett t)
Definition: value_set_analysis.h:43
static_analysis_baset::ns
const namespacet & ns
Definition: static_analysis.h:178