cprover
Loading...
Searching...
No Matches
value_set_analysis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Propagation
4
5Author: 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
21class 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
36template<class VSDT>
38 public value_setst,
39 public static_analysist<VSDT>
40{
41public:
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;
62 goto_program,
63 dest);
64 }
65
66public:
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
75typedef
78
79void convert(
80 const goto_functionst &goto_functions,
82 xmlt &dest);
83
84void convert(
85 const goto_programt &goto_program,
87 xmlt &dest);
88
89#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
goto_programt::const_targett locationt
Definition ai.h:587
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.
instructionst::const_iterator const_targett
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
This template class implements a data-flow analysis which keeps track of what values different variab...
const value_sett & get_value_set(goto_programt::const_targett t)
void convert(const goto_programt &goto_program, xmlt &dest) const
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.