cprover
invariant_propagation.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Invariant Propagation
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
13
#define CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
14
15
#include <
pointer-analysis/value_sets.h
>
16
17
#include "
ai.h
"
18
#include "
invariant_set_domain.h
"
19
20
class
invariant_set_domain_factoryt
;
21
22
class
invariant_propagationt
:
public
23
ait
<invariant_set_domaint>
24
{
25
public
:
26
invariant_propagationt
(
const
namespacet
&_ns,
value_setst
&_value_sets);
27
28
const
invariant_sett
&
lookup
(
locationt
l)
const
29
{
30
return
(*
this
)[l].invariant_set;
31
}
32
33
void
initialize
(
const
irep_idt
&
function
,
const
goto_programt
&goto_program)
34
override
;
35
36
void
make_all_true
();
37
void
make_all_false
();
38
39
void
simplify
(
goto_programt
&goto_program);
40
void
simplify
(
goto_functionst
&goto_functions);
41
42
typedef
ait<invariant_set_domaint>
baset
;
43
44
protected
:
45
// Each invariant_set_domain needs access to a few of the fields of the
46
// invariant_propagation object. This is a historic design that predates
47
// the current interfaces. Removing it would require a substantial refactor.
48
// A minimally-intrusive work around is for the domain factory to be a
49
// friend of the analyser object and create domains with references to the
50
// relevant fields.
51
friend
invariant_set_domain_factoryt
;
52
53
const
namespacet
&
ns
;
54
value_setst
&
value_sets
;
55
56
inv_object_storet
object_store
;
57
58
typedef
std::list<unsigned>
object_listt
;
59
60
void
add_objects
(
const
goto_programt
&goto_program);
61
void
add_objects
(
const
goto_functionst
&goto_functions);
62
63
void
get_objects
(
64
const
symbolt
&symbol,
65
object_listt
&dest);
66
67
void
get_objects_rec
(
68
const
exprt
&src,
69
std::list<exprt> &dest);
70
71
void
get_globals
(
object_listt
&globals);
72
73
bool
check_type
(
const
typet
&type)
const
;
74
};
75
76
#endif // CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
inv_object_storet
Definition:
invariant_set.h:25
ai_baset::locationt
goto_programt::const_targett locationt
Definition:
ai.h:126
invariant_set_domain.h
Value Set.
invariant_propagationt::object_listt
std::list< unsigned > object_listt
Definition:
invariant_propagation.h:58
typet
The type of an expression, extends irept.
Definition:
type.h:29
invariant_set_domain_factoryt
Pass the necessary arguments to the invariant_set_domaint's when constructed.
Definition:
invariant_propagation.cpp:21
invariant_propagationt::ns
const namespacet & ns
Definition:
invariant_propagation.h:53
invariant_propagationt::invariant_set_domain_factoryt
friend invariant_set_domain_factoryt
Definition:
invariant_propagation.h:51
exprt
Base class for all expressions.
Definition:
expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition:
ai.h:558
invariant_propagationt::make_all_true
void make_all_true()
Definition:
invariant_propagation.cpp:51
invariant_propagationt::get_objects
void get_objects(const symbolt &symbol, object_listt &dest)
Definition:
invariant_propagation.cpp:113
invariant_propagationt::make_all_false
void make_all_false()
Definition:
invariant_propagation.cpp:59
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:92
invariant_propagationt::get_objects_rec
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Definition:
invariant_propagation.cpp:125
invariant_propagationt::add_objects
void add_objects(const goto_programt &goto_program)
Definition:
invariant_propagation.cpp:67
invariant_propagationt::check_type
bool check_type(const typet &type) const
Definition:
invariant_propagation.cpp:220
invariant_propagationt::invariant_propagationt
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
Definition:
invariant_propagation.cpp:40
invariant_propagationt::get_globals
void get_globals(object_listt &globals)
Definition:
invariant_propagation.cpp:207
invariant_propagationt::simplify
void simplify(goto_programt &goto_program)
Definition:
invariant_propagation.cpp:254
invariant_propagationt::lookup
const invariant_sett & lookup(locationt l) const
Definition:
invariant_propagation.h:28
ai.h
Abstract Interpretation.
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
value_setst
Definition:
value_sets.h:22
invariant_sett
Definition:
invariant_set.h:75
invariant_propagationt::baset
ait< invariant_set_domaint > baset
Definition:
invariant_propagation.h:42
symbolt
Symbol table entry.
Definition:
symbol.h:28
invariant_propagationt::value_sets
value_setst & value_sets
Definition:
invariant_propagation.h:54
invariant_propagationt::object_store
inv_object_storet object_store
Definition:
invariant_propagation.h:56
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:73
invariant_propagationt
Definition:
invariant_propagation.h:24
invariant_propagationt::initialize
void initialize(const irep_idt &function, const goto_programt &goto_program) override
Initialize all the abstract states for a single function.
Definition:
invariant_propagation.cpp:239
analyses
invariant_propagation.h
Generated by
1.8.20