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 
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 
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
The type of an expression.
Definition: type.h:22
std::list< unsigned > object_listt
goto_programt::const_targett locationt
Definition: ai.h:132
Definition: ai.h:377
void get_objects(const symbolt &symbol, object_listt &dest)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
bool check_type(const typet &type) const
virtual void initialize(const goto_programt &goto_program)
Value Set Propagation.
void add_objects(const goto_programt &goto_program)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void get_globals(object_listt &globals)
const invariant_sett & lookup(locationt l) const
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
Abstract Interpretation.
void simplify(goto_programt &goto_program)
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
inv_object_storet object_store
ait< invariant_set_domaint > baset