cprover
value_set_analysis_fi.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Value Set Propagation (flow insensitive)
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
13
#define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
14
15
#include <
analyses/flow_insensitive_analysis.h
>
16
17
#include "
value_set_domain_fi.h
"
18
#include "
value_sets.h
"
19
20
class
value_set_analysis_fit
:
21
public
value_setst
,
22
public
flow_insensitive_analysist
<value_set_domain_fit>
23
{
24
public
:
25
enum
track_optionst
{
TRACK_ALL_POINTERS
,
TRACK_FUNCTION_POINTERS
};
26
27
// constructor
28
value_set_analysis_fit
(
29
const
namespacet
&_ns,
30
track_optionst
_track_options=
TRACK_ALL_POINTERS
):
31
flow_insensitive_analysist
<
value_set_domain_fit
>(_ns),
32
track_options
(_track_options)
33
{
34
}
35
36
typedef
flow_insensitive_analysist<value_set_domain_fit>
baset
;
37
38
void
initialize
(
const
goto_programt
&goto_program)
override
;
39
void
initialize
(
const
goto_functionst
&goto_functions)
override
;
40
41
protected
:
42
track_optionst
track_options
;
43
44
bool
check_type
(
const
typet
&type);
45
void
get_globals
(std::list<value_set_fit::entryt> &dest);
46
void
add_vars
(
const
goto_functionst
&goto_functions);
47
void
add_vars
(
const
goto_programt
&goto_programa);
48
49
void
get_entries
(
50
const
symbolt
&symbol,
51
std::list<value_set_fit::entryt> &dest);
52
53
void
get_entries_rec
(
54
const
irep_idt
&identifier,
55
const
std::string &suffix,
56
const
typet
&type,
57
std::list<value_set_fit::entryt> &dest);
58
59
public
:
60
// interface value_sets
61
std::vector<exprt>
get_values
(
62
const
irep_idt
&function_id,
63
locationt
l,
64
const
exprt
&expr)
override
;
65
};
66
67
#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
value_set_analysis_fit::baset
flow_insensitive_analysist< value_set_domain_fit > baset
Definition:
value_set_analysis_fi.h:36
typet
The type of an expression, extends irept.
Definition:
type.h:28
value_set_analysis_fit::get_entries_rec
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
Definition:
value_set_analysis_fi.cpp:86
value_set_analysis_fit::value_set_analysis_fit
value_set_analysis_fit(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
Definition:
value_set_analysis_fi.h:28
exprt
Base class for all expressions.
Definition:
expr.h:54
value_set_analysis_fit
Definition:
value_set_analysis_fi.h:23
value_sets.h
Value Set Propagation.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:91
value_set_analysis_fit::initialize
void initialize(const goto_programt &goto_program) override
Definition:
value_set_analysis_fi.cpp:17
value_set_domain_fi.h
Value Set (Flow Insensitive)
value_set_analysis_fit::get_globals
void get_globals(std::list< value_set_fit::entryt > &dest)
Definition:
value_set_analysis_fi.cpp:140
value_set_analysis_fit::track_optionst
track_optionst
Definition:
value_set_analysis_fi.h:25
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
value_set_analysis_fit::check_type
bool check_type(const typet &type)
Definition:
value_set_analysis_fi.cpp:153
value_set_analysis_fit::get_values
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
Definition:
value_set_analysis_fi.cpp:194
value_set_analysis_fit::TRACK_FUNCTION_POINTERS
@ TRACK_FUNCTION_POINTERS
Definition:
value_set_analysis_fi.h:25
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:25
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition:
flow_insensitive_analysis.h:94
value_setst
Definition:
value_sets.h:22
symbolt
Symbol table entry.
Definition:
symbol.h:28
value_set_analysis_fit::get_entries
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
Definition:
value_set_analysis_fi.cpp:79
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:71
value_set_domain_fit
Definition:
value_set_domain_fi.h:21
value_set_analysis_fit::track_options
track_optionst track_options
Definition:
value_set_analysis_fi.h:42
value_set_analysis_fit::add_vars
void add_vars(const goto_functionst &goto_functions)
Definition:
value_set_analysis_fi.cpp:113
value_set_analysis_fit::TRACK_ALL_POINTERS
@ TRACK_ALL_POINTERS
Definition:
value_set_analysis_fi.h:25
flow_insensitive_analysist
Definition:
flow_insensitive_analysis.h:232
pointer-analysis
value_set_analysis_fi.h
Generated by
1.8.20