12 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 13 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 56 replace_const.
clear();
62 replace_const.
expr_map[lhs_id] = rhs_val;
83 replace_const.
clear();
116 operator()(goto_functions, ns);
117 replace(goto_functions, ns);
124 operator()(goto_function, ns);
125 replace(goto_function, ns);
131 void replace_array_symbol(
142 void replace_types_rec(
148 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H void assign(valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const
bool is_array_constant(const exprt &expr) const
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
bool is_constant_address_of(const exprt &expr) const
void transform(locationt, locationt, ai_baset &, const namespacet &) final
const irep_idt & get_identifier() const
bool meet(const valuest &src)
meet
bool merge(const valuest &src)
join
bool is_constant(const exprt &expr) const
constant_propagator_ait(goto_functionst::goto_functiont &goto_function, const namespacet &ns)
void set_to(const symbol_exprt &lhs, const exprt &rhs_val)
goto_function_templatet< goto_programt > goto_functiont
constant_propagator_ait(goto_functionst &goto_functions, const namespacet &ns)
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns)
handles equalities and conjunctions containing equalities
Modified expression replacement for constant propagator.
bool set_to_top(const irep_idt &id)
Do not call this when iterating over replace_const.expr_map!
Base class for all expressions.
void output(std::ostream &, const namespacet &) const
bool set_to_top(const symbol_exprt &expr)
void set_to(const irep_idt &lhs_id, const exprt &rhs_val)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
bool merge(const constant_propagator_domaint &, locationt, locationt)
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
void output(std::ostream &, const ai_baset &, const namespacet &) const final
replace_symbol_extt replace_const