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  std::vector<exprt>
69  get_values(const irep_idt &, locationt l, const exprt &expr) override
70  {
71  return (*this)[l].value_set.get_value_set(expr, baset::ns);
72  }
73 };
74 
75 typedef
78 
79 void convert(
80  const goto_functionst &goto_functions,
81  const value_set_analysist &value_set_analysis,
82  xmlt &dest);
83 
84 void convert(
85  const goto_programt &goto_program,
86  const value_set_analysist &value_set_analysis,
87  xmlt &dest);
88 
89 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const namespacet & ns
goto_programt::const_targett locationt
goto_programt::const_targett locationt
This template class implements a data-flow analysis which keeps track of what values different variab...
void convert(const goto_programt &goto_program, xmlt &dest) const
const value_sett & get_value_set(goto_programt::const_targett t)
value_set_analysis_templatet(const namespacet &ns)
static_analysist< domaint > baset
std::vector< exprt > get_values(const irep_idt &, locationt l, const exprt &expr) override
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:43
Definition: xml.h:21
Static Analysis.
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
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)
Value Set Propagation.