Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
13 #define CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
21 ait<invariant_set_domaint>
36 return (*
this)[l].invariant_set;
67 std::list<exprt> &dest);
74 #endif // CPROVER_ANALYSES_INVARIANT_PROPAGATION_H
goto_programt::const_targett locationt
std::list< unsigned > object_listt
The type of an expression, extends irept.
Base class for all expressions.
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
void get_objects(const symbolt &symbol, object_listt &dest)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
void add_objects(const goto_programt &goto_program)
bool check_type(const typet &type) const
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
void get_globals(object_listt &globals)
void simplify(goto_programt &goto_program)
const invariant_sett & lookup(locationt l) const
A collection of goto functions.
ait< invariant_set_domaint > baset
inv_object_storet object_store
A generic container class for the GOTO intermediate representation of one function.