cprover
|
#include <constant_propagator.h>
Classes | |
struct | valuest |
Public Member Functions | |
void | transform (locationt, locationt, ai_baset &, const namespacet &) final |
void | output (std::ostream &, const ai_baset &, const namespacet &) const final |
void | make_top () final |
void | make_bottom () final |
void | make_entry () final |
bool | merge (const constant_propagator_domaint &, locationt, locationt) |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const override |
Simplify the condition given context-sensitive knowledge from the abstract state. More... | |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
virtual jsont | output_json (const ai_baset &ai, const namespacet &ns) const |
virtual xmlt | output_xml (const ai_baset &ai, const namespacet &ns) const |
virtual bool | ai_simplify_lhs (exprt &condition, const namespacet &ns) const |
Use the information in the domain to simplify the expression on the LHS of an assignment. More... | |
Public Attributes | |
valuest | values |
Private Member Functions | |
void | assign (valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const |
void | assign_rec (valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns) |
bool | two_way_propagate_rec (const exprt &expr, const namespacet &ns) |
handles equalities and conjunctions containing equalities More... | |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 19 of file constant_propagator.h.
|
overridevirtual |
Simplify the condition given context-sensitive knowledge from the abstract state.
Reimplemented from ai_domain_baset.
Definition at line 270 of file constant_propagator.cpp.
References replace_symbol_extt::replace(), constant_propagator_domaint::valuest::replace_const, simplify(), and values.
|
private |
Definition at line 255 of file constant_propagator.cpp.
References constant_propagator_domaint::valuest::replace_const, constant_propagator_domaint::valuest::set_to(), simplify_expr(), and values.
Referenced by assign_rec().
|
private |
Definition at line 53 of file constant_propagator.cpp.
References assign(), concatenate_array_id(), namespace_baset::follow(), forall_operands, from_expr(), from_type(), irept::id(), constant_propagator_domaint::valuest::is_constant(), exprt::op0(), exprt::op1(), exprt::operands(), constant_propagator_domaint::valuest::replace_const, constant_propagator_domaint::valuest::set_to_top(), simplify_expr(), to_symbol_expr(), exprt::type(), and values.
Referenced by transform(), and two_way_propagate_rec().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 32 of file constant_propagator.h.
References constant_propagator_domaint::valuest::set_to_bottom(), and values.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 33 of file constant_propagator.h.
References constant_propagator_domaint::valuest::set_to_top(), and values.
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 31 of file constant_propagator.h.
References constant_propagator_domaint::valuest::set_to_top(), and values.
bool constant_propagator_domaint::merge | ( | const constant_propagator_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 459 of file constant_propagator.cpp.
References constant_propagator_domaint::valuest::merge(), and values.
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 371 of file constant_propagator.cpp.
References constant_propagator_domaint::valuest::output(), and values.
Referenced by transform().
|
final |
Definition at line 124 of file constant_propagator.cpp.
References assign_rec(), code_function_callt::function(), symbol_exprt::get_identifier(), exprt::is_constant(), exprt::is_false(), code_assignt::lhs(), output(), code_assignt::rhs(), constant_propagator_domaint::valuest::set_to_bottom(), constant_propagator_domaint::valuest::set_to_top(), simplify_expr(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), to_symbol_expr(), two_way_propagate_rec(), and values.
|
private |
handles equalities and conjunctions containing equalities
Definition at line 214 of file constant_propagator.cpp.
References assign_rec(), forall_operands, from_expr(), irept::id(), constant_propagator_domaint::valuest::is_constant(), constant_propagator_domaint::valuest::meet(), exprt::op0(), exprt::op1(), and values.
Referenced by transform().
valuest constant_propagator_domaint::values |
Definition at line 89 of file constant_propagator.h.
Referenced by ai_simplify(), assign(), assign_rec(), make_bottom(), make_entry(), make_top(), merge(), output(), transform(), and two_way_propagate_rec().