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  public value_setst,
25  public static_analysist<value_set_domaint>
26 {
27 public:
28  explicit value_set_analysist(const namespacet &_ns):
30  {
31  }
32 
34 
35  // overloading
36  virtual void initialize(const goto_programt &goto_program);
37  virtual void initialize(const goto_functionst &goto_functions);
38 
39  void convert(
40  const goto_programt &goto_program,
41  const irep_idt &identifier,
42  xmlt &dest) const;
43 
44 public:
45  // interface value_sets
46  virtual void get_values(
47  locationt l,
48  const exprt &expr,
50  {
51  (*this)[l].value_set.get_value_set(expr, dest, ns);
52  }
53 };
54 
55 void convert(
56  const goto_functionst &goto_functions,
57  const value_set_analysist &value_set_analysis,
58  xmlt &dest);
59 
60 void convert(
61  const goto_programt &goto_program,
62  const value_set_analysist &value_set_analysis,
63  xmlt &dest);
64 
65 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
const namespacet & ns
static_analysist< value_set_domaint > baset
Value Set Propagation.
virtual void get_values(locationt l, const exprt &expr, value_setst::valuest &dest)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
goto_programt::const_targett locationt
Definition: xml.h:18
void convert(const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
virtual void initialize(const goto_programt &goto_program)
Static Analysis.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Base class for all expressions.
Definition: expr.h:46
std::list< exprt > valuest
Definition: value_sets.h:28
value_set_analysist(const namespacet &_ns)