cprover
Loading...
Searching...
No Matches
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 "
ai.h
"
16
#include "
invariant_set_domain.h
"
17
18
class
invariant_set_domain_factoryt
;
19
class
value_setst
;
20
21
class
invariant_propagationt
:
public
22
ait
<invariant_set_domaint>
23
{
24
public
:
25
invariant_propagationt
(
const
namespacet
&_ns,
value_setst
&_value_sets);
26
27
const
invariant_sett
&
lookup
(
locationt
l)
const
28
{
29
return
(*
this
)[l].invariant_set;
30
}
31
32
void
initialize
(
const
irep_idt
&function,
const
goto_programt
&goto_program)
33
override
;
34
35
void
make_all_true
();
36
void
make_all_false
();
37
38
void
simplify
(
goto_programt
&goto_program);
39
void
simplify
(
goto_functionst
&goto_functions);
40
41
typedef
ait<invariant_set_domaint>
baset
;
42
43
protected
:
44
// Each invariant_set_domain needs access to a few of the fields of the
45
// invariant_propagation object. This is a historic design that predates
46
// the current interfaces. Removing it would require a substantial refactor.
47
// A minimally-intrusive work around is for the domain factory to be a
48
// friend of the analyser object and create domains with references to the
49
// relevant fields.
50
friend
invariant_set_domain_factoryt
;
51
52
const
namespacet
&
ns
;
53
value_setst
&
value_sets
;
54
55
inv_object_storet
object_store
;
56
57
typedef
std::list<unsigned>
object_listt
;
58
59
void
add_objects
(
const
goto_programt
&goto_program);
60
void
add_objects
(
const
goto_functionst
&goto_functions);
61
62
void
get_objects
(
63
const
symbolt
&symbol,
64
object_listt
&dest);
65
66
void
get_objects_rec
(
67
const
exprt
&src,
68
std::list<exprt> &dest);
69
70
void
get_globals
(
object_listt
&globals);
71
72
bool
check_type
(
const
typet
&type)
const
;
73
};
74
75
#endif
// CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
ai.h
Abstract Interpretation.
ait< invariant_set_domaint >::locationt
goto_programt::const_targett locationt
Definition
ai.h:585
ait< invariant_set_domaint >::ait
ait()
Definition
ai.h:565
exprt
Base class for all expressions.
Definition
expr.h:56
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:73
inv_object_storet
Definition
invariant_set.h:30
invariant_propagationt::value_sets
value_setst & value_sets
Definition
invariant_propagation.h:53
invariant_propagationt::ns
const namespacet & ns
Definition
invariant_propagation.h:52
invariant_propagationt::invariant_set_domain_factoryt
friend invariant_set_domain_factoryt
Definition
invariant_propagation.h:50
invariant_propagationt::add_objects
void add_objects(const goto_programt &goto_program)
Definition
invariant_propagation.cpp:66
invariant_propagationt::simplify
void simplify(goto_programt &goto_program)
Definition
invariant_propagation.cpp:258
invariant_propagationt::make_all_true
void make_all_true()
Definition
invariant_propagation.cpp:50
invariant_propagationt::make_all_false
void make_all_false()
Definition
invariant_propagation.cpp:58
invariant_propagationt::get_objects
void get_objects(const symbolt &symbol, object_listt &dest)
Definition
invariant_propagation.cpp:112
invariant_propagationt::lookup
const invariant_sett & lookup(locationt l) const
Definition
invariant_propagation.h:27
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:243
invariant_propagationt::get_objects_rec
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Definition
invariant_propagation.cpp:124
invariant_propagationt::object_listt
std::list< unsigned > object_listt
Definition
invariant_propagation.h:57
invariant_propagationt::object_store
inv_object_storet object_store
Definition
invariant_propagation.h:55
invariant_propagationt::check_type
bool check_type(const typet &type) const
Definition
invariant_propagation.cpp:222
invariant_propagationt::get_globals
void get_globals(object_listt &globals)
Definition
invariant_propagation.cpp:209
invariant_propagationt::invariant_propagationt
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
Definition
invariant_propagation.cpp:39
invariant_propagationt::baset
ait< invariant_set_domaint > baset
Definition
invariant_propagation.h:41
invariant_set_domain_factoryt
Pass the necessary arguments to the invariant_set_domaint's when constructed.
Definition
invariant_propagation.cpp:20
invariant_sett
Definition
invariant_set.h:80
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:94
symbolt
Symbol table entry.
Definition
symbol.h:28
typet
The type of an expression, extends irept.
Definition
type.h:29
value_setst
Definition
value_sets.h:22
invariant_set_domain.h
Value Set.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
analyses
invariant_propagation.h
Generated by
1.13.1