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 The type of an expression.
std::list< unsigned > object_listt
goto_programt::const_targett locationt
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...
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)
void add_objects(const goto_programt &goto_program)
void get_globals(object_listt &globals)
const invariant_sett & lookup(locationt l) const
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
void simplify(goto_programt &goto_program)
Base class for all expressions.
inv_object_storet object_store
ait< invariant_set_domaint > baset