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  std::function<const value_sett &(goto_programt::const_targett)> get_value_set,
26  const irep_idt &identifier,
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 
43  void convert(
45  const irep_idt &identifier,
46  xmlt &dest) const
47  {
49  [this](locationt l) { return (*this)[l].value_set; },
51  identifier,
52  dest);
53  }
54 
55 public:
56  // interface value_sets
57  virtual void get_values(
58  locationt l,
59  const exprt &expr,
61  {
62  (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
63  }
64 };
65 
66 typedef
69 
70 void convert(
71  const goto_functionst &goto_functions,
72  const value_set_analysist &value_set_analysis,
73  xmlt &dest);
74 
75 void convert(
77  const value_set_analysist &value_set_analysis,
78  xmlt &dest);
79 
80 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
const namespacet & ns
value_set_analysis_templatet(const namespacet &ns)
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)
goto_programt::const_targett locationt
Value Set Propagation.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
goto_programt::const_targett locationt
Definition: xml.h:18
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:70
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
void convert(const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
void value_sets_to_xml(std::function< const value_sett &(goto_programt::const_targett)> get_value_set, const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest)
std::list< exprt > valuest
Definition: value_sets.h:28
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist