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
Abstract Interpretation.
goto_programt::const_targett locationt
Definition: ai.h:127
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
void add_objects(const goto_programt &goto_program)
void simplify(goto_programt &goto_program)
void get_objects(const symbolt &symbol, object_listt &dest)
const invariant_sett & lookup(locationt l) const
void initialize(const irep_idt &function, const goto_programt &goto_program) override
Initialize all the abstract states for a single function.
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
std::list< unsigned > object_listt
inv_object_storet object_store
bool check_type(const typet &type) const
void get_globals(object_listt &globals)
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
ait< invariant_set_domaint > baset
Pass the necessary arguments to the invariant_set_domaint's when constructed.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
Value Set Propagation.