cprover
|
#include <constant_propagator.h>
Public Member Functions | |
valuest () | |
bool | merge (const valuest &src) |
join More... | |
bool | meet (const valuest &src) |
meet More... | |
void | set_to_bottom () |
void | set_to_top () |
bool | is_bot () const |
bool | is_top () const |
void | set_to (const irep_idt &lhs, const exprt &rhs) |
void | set_to (const symbol_exprt &lhs, const exprt &rhs) |
bool | set_to_top (const symbol_exprt &expr) |
bool | set_to_top (const irep_idt &id) |
Do not call this when iterating over replace_const.expr_map! More... | |
void | set_dirty_to_top (const dirtyt &dirty, const namespacet &ns) |
bool | is_constant (const exprt &expr) const |
bool | is_array_constant (const exprt &expr) const |
bool | is_constant_address_of (const exprt &expr) const |
bool | is_empty () const |
void | output (std::ostream &out, const namespacet &ns) const |
Public Attributes | |
replace_symbolt | replace_const |
bool | is_bottom |
Definition at line 69 of file constant_propagator.h.
|
inline |
Definition at line 72 of file constant_propagator.h.
bool constant_propagator_domaint::valuest::is_array_constant | ( | const exprt & | expr | ) | const |
|
inline |
Definition at line 95 of file constant_propagator.h.
References replace_symbolt::empty(), is_bottom, and replace_const.
Referenced by constant_propagator_domaint::is_bottom().
bool constant_propagator_domaint::valuest::is_constant | ( | const exprt & | expr | ) | const |
Definition at line 279 of file constant_propagator.cpp.
References replace_symbolt::expr_map, forall_operands, side_effect_exprt::get_statement(), irept::id(), is_constant_address_of(), address_of_exprt::object(), replace_const, to_address_of_expr(), to_side_effect_expr(), and to_symbol_expr().
Referenced by constant_propagator_domaint::partial_evaluate(), and constant_propagator_domaint::two_way_propagate_rec().
bool constant_propagator_domaint::valuest::is_constant_address_of | ( | const exprt & | expr | ) | const |
Definition at line 307 of file constant_propagator.cpp.
References index_exprt::array(), irept::id(), index_exprt::index(), dereference_exprt::pointer(), member_exprt::struct_op(), to_dereference_expr(), to_index_expr(), and to_member_expr().
Referenced by is_constant().
|
inline |
Definition at line 131 of file constant_propagator.h.
References replace_symbolt::expr_map, and replace_const.
|
inline |
Definition at line 100 of file constant_propagator.h.
References replace_symbolt::empty(), is_bottom, and replace_const.
Referenced by constant_propagator_domaint::is_top().
bool constant_propagator_domaint::valuest::meet | ( | const valuest & | src | ) |
meet
Definition at line 467 of file constant_propagator.cpp.
References replace_symbolt::expr_map, constant_propagator_domaint::is_bottom(), is_bottom, and replace_const.
Referenced by constant_propagator_domaint::two_way_propagate_rec().
bool constant_propagator_domaint::valuest::merge | ( | const valuest & | src | ) |
join
Definition at line 397 of file constant_propagator.cpp.
References replace_symbolt::expr_map, irept::find(), INVARIANT, constant_propagator_domaint::is_bottom(), is_bottom, PRECONDITION, and replace_const.
Referenced by constant_propagator_domaint::merge().
void constant_propagator_domaint::valuest::output | ( | std::ostream & | out, |
const namespacet & | ns | ||
) | const |
Definition at line 360 of file constant_propagator.cpp.
References DATA_INVARIANT, from_expr(), INVARIANT, and constant_propagator_domaint::is_bottom().
Referenced by constant_propagator_domaint::output().
void constant_propagator_domaint::valuest::set_dirty_to_top | ( | const dirtyt & | dirty, |
const namespacet & | ns | ||
) |
Definition at line 338 of file constant_propagator.cpp.
References irept::get_bool(), symbolt::is_procedure_local(), namespacet::lookup(), and symbolt::type.
Referenced by constant_propagator_domaint::transform().
|
inline |
Definition at line 107 of file constant_propagator.h.
References replace_symbolt::expr_map, is_bottom, and replace_const.
Referenced by constant_propagator_domaint::assign_rec(), constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(), and set_to().
|
inline |
Definition at line 113 of file constant_propagator.h.
References symbol_exprt::get_identifier(), and set_to().
|
inline |
Definition at line 83 of file constant_propagator.h.
References replace_symbolt::clear(), is_bottom, and replace_const.
Referenced by constant_propagator_domaint::make_bottom(), and constant_propagator_domaint::transform().
|
inline |
Definition at line 89 of file constant_propagator.h.
References replace_symbolt::clear(), is_bottom, and replace_const.
Referenced by constant_propagator_domaint::assign_rec(), constant_propagator_domaint::make_top(), set_to_top(), and constant_propagator_domaint::transform().
|
inline |
Definition at line 118 of file constant_propagator.h.
References symbol_exprt::get_identifier(), and set_to_top().
bool constant_propagator_domaint::valuest::set_to_top | ( | const irep_idt & | id | ) |
Do not call this when iterating over replace_const.expr_map!
Definition at line 327 of file constant_propagator.cpp.
References INVARIANT, constant_propagator_domaint::is_bottom(), and size_type().
bool constant_propagator_domaint::valuest::is_bottom |
Definition at line 76 of file constant_propagator.h.
Referenced by is_bot(), is_top(), meet(), merge(), set_to(), set_to_bottom(), set_to_top(), and constant_propagator_domaint::transform().
replace_symbolt constant_propagator_domaint::valuest::replace_const |
Definition at line 75 of file constant_propagator.h.
Referenced by is_bot(), is_constant(), is_empty(), is_top(), meet(), merge(), constant_propagator_domaint::replace_constants_and_simplify(), set_to(), set_to_bottom(), and set_to_top().