22 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 23 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 78 virtual bool is_top() const final
override 165 typedef std::function<bool(const exprt &, const namespacet &)>
176 dirty(goto_functions),
184 dirty(goto_function),
192 dirty(goto_model.goto_functions),
201 const irep_idt &function_identifier,
207 operator()(function_identifier, goto_function, ns);
231 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
bool is_array_constant(const exprt &expr) const
void assign_rec(valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp)
bool is_constant_address_of(const exprt &expr) const
Variables whose address is taken.
bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const
void replace_types_rec(const replace_symbolt &replace_const, exprt &expr)
void set_to(const symbol_exprt &lhs, const exprt &rhs)
virtual bool is_top() const final override
symbol_tablet symbol_table
Symbol table.
bool merge(const valuest &src)
join
void operator()(const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
bool is_constant(const exprt &expr) const
constant_propagator_ait(const goto_functionst &goto_functions, should_track_valuet should_track_value=track_all_values)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Replace expression or type symbols by an expression or type, respectively.
constant_propagator_ait(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
Replace symbols with constants while maintaining syntactically valid expressions. ...
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
should_track_valuet should_track_value
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const final override
Simplify the condition given context-sensitive knowledge from the abstract state. ...
virtual void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it...
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai_base, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
virtual bool is_bottom() const final override
virtual void make_bottom() final override
no states
std::function< bool(const exprt &, const namespacet &)> should_track_valuet
bool partial_evaluate_with_all_rounding_modes(exprt &expr, const namespacet &ns) const
Attempt to evaluate an expression in all rounding modes.
virtual void output(std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override
void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns)
address_of_aware_replace_symbolt replace_const
The basic interface of an abstract interpreter.
Base class for all expressions.
virtual void make_entry() final override
Make this domain a reasonable entry-point state.
constant_propagator_ait(goto_modelt &goto_model, should_track_valuet should_track_value=track_all_values)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
void replace(goto_functionst::goto_functiont &, const namespacet &)
goto_functionst goto_functions
GOTO functions.
void output(std::ostream &out, const namespacet &ns) const
static bool track_all_values(const exprt &, const namespacet &)
bool meet(const valuest &src, const namespacet &ns)
meet
bool merge(const constant_propagator_domaint &other, locationt from, locationt to)