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  ait<invariant_set_domaint>
22 {
23 public:
25  const namespacet &_ns,
26  value_setst &_value_sets):
28  ns(_ns),
29  value_sets(_value_sets),
30  object_store(_ns)
31  {
32  }
33 
35  {
36  return (*this)[l].invariant_set;
37  }
38 
39  virtual void initialize(const goto_programt &goto_program);
40  virtual void initialize(const goto_functionst &goto_functions);
41 
42  void make_all_true();
43  void make_all_false();
44 
45  void simplify(goto_programt &goto_program);
46  void simplify(goto_functionst &goto_functions);
47 
49 
50 protected:
51  const namespacet &ns;
53 
55 
56  typedef std::list<unsigned> object_listt;
57 
58  void add_objects(const goto_programt &goto_program);
59  void add_objects(const goto_functionst &goto_functions);
60 
61  void get_objects(
62  const symbolt &symbol,
63  object_listt &dest);
64 
65  void get_objects_rec(
66  const exprt &src,
67  std::list<exprt> &dest);
68 
69  void get_globals(object_listt &globals);
70 
71  bool check_type(const typet &type) const;
72 };
73 
74 #endif // CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
invariant_set_domaint
Definition: invariant_set_domain.h:20
inv_object_storet
Definition: invariant_set.h:25
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:36
invariant_set_domain.h
invariant_propagationt::object_listt
std::list< unsigned > object_listt
Definition: invariant_propagation.h:56
typet
The type of an expression, extends irept.
Definition: type.h:27
invariant_propagationt::ns
const namespacet & ns
Definition: invariant_propagation.h:51
exprt
Base class for all expressions.
Definition: expr.h:54
ait
Definition: ai.h:365
invariant_propagationt::make_all_true
void make_all_true()
Definition: invariant_propagation.cpp:19
invariant_propagationt::initialize
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: invariant_propagation.cpp:203
invariant_propagationt::get_objects
void get_objects(const symbolt &symbol, object_listt &dest)
Definition: invariant_propagation.cpp:77
invariant_propagationt::make_all_false
void make_all_false()
Definition: invariant_propagation.cpp:25
value_sets.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
invariant_propagationt::get_objects_rec
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Definition: invariant_propagation.cpp:89
invariant_propagationt::add_objects
void add_objects(const goto_programt &goto_program)
Definition: invariant_propagation.cpp:31
invariant_propagationt::check_type
bool check_type(const typet &type) const
Definition: invariant_propagation.cpp:183
invariant_propagationt::invariant_propagationt
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
Definition: invariant_propagation.h:24
invariant_propagationt::get_globals
void get_globals(object_listt &globals)
Definition: invariant_propagation.cpp:170
invariant_propagationt::simplify
void simplify(goto_programt &goto_program)
Definition: invariant_propagation.cpp:238
invariant_propagationt::lookup
const invariant_sett & lookup(locationt l) const
Definition: invariant_propagation.h:34
ai.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
value_setst
Definition: value_sets.h:21
invariant_sett
Definition: invariant_set.h:77
invariant_propagationt::baset
ait< invariant_set_domaint > baset
Definition: invariant_propagation.h:48
symbolt
Symbol table entry.
Definition: symbol.h:27
invariant_propagationt::value_sets
value_setst & value_sets
Definition: invariant_propagation.h:52
invariant_propagationt::object_store
inv_object_storet object_store
Definition: invariant_propagation.h:54
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
invariant_propagationt
Definition: invariant_propagation.h:20