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 
16 
17 #include "ai.h"
18 #include "invariant_set_domain.h"
19 
21 
23  ait<invariant_set_domaint>
24 {
25 public:
26  invariant_propagationt(const namespacet &_ns, value_setst &_value_sets);
27 
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 
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.
52 
53  const namespacet &ns;
55 
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