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
const namespacet & ns
value_set_analysis_templatet(const namespacet &ns)
void convert(const goto_programt &goto_program, xmlt &dest) const
virtual void get_values(locationt l, const exprt &expr, value_setst::valuest &dest)
static_analysist< domaint > baset
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
const value_sett & get_value_set(goto_programt::const_targett t)
goto_programt::const_targett locationt
Value Set Propagation.
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_programt::const_targett locationt
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: xml.h:18
A collection of goto functions.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
Static Analysis.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Base class for all expressions.
Definition: expr.h:54
std::list< exprt > valuest
Definition: value_sets.h:28
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist