12 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 13 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H 66 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),
204 dirty(goto_function),
231 #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
bool is_array_constant(const exprt &expr) const
virtual void transform(locationt from, 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...
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)
const irep_idt & get_identifier() const
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
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...
bool partial_evaluate(exprt &expr, const namespacet &ns) const
Attempt to evaluate expression using domain knowledge This function changes the expression that is pa...
constant_propagator_ait(goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value=track_all_values)
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...
::goto_functiont goto_functiont
constant_propagator_ait(const goto_functiont &goto_function, should_track_valuet should_track_value=track_all_values)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
replace_symbolt replace_const
bool two_way_propagate_rec(const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp)
handles equalities and conjunctions containing equalities
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)
void operator()(const goto_programt &goto_program, const namespacet &ns)
Running the interpreter.
The basic interface of an abstract interpreter.
Base class for all expressions.
virtual void make_entry() final override
a reasonable entry-point state
bool set_to_top(const symbol_exprt &expr)
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 set_to(const irep_idt &lhs, const exprt &rhs)
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)