CBMC
|
#include <constant_propagator.h>
Public Member Functions | |
bool | merge (const valuest &src) |
join | |
bool | meet (const valuest &src, const namespacet &ns) |
meet | |
void | set_to_bottom () |
void | set_to_top () |
bool | is_bot () const |
bool | is_top () const |
void | set_to (const symbol_exprt &lhs, const exprt &rhs) |
bool | set_to_top (const symbol_exprt &expr) |
Do not call this when iterating over replace_const.expr_map! | |
void | set_dirty_to_top (const dirtyt &dirty, const namespacet &ns) |
bool | is_constant (const exprt &expr, const namespacet &ns) const |
bool | is_constant (const irep_idt &id, const namespacet &ns) const |
bool | is_empty () const |
void | output (std::ostream &out, const namespacet &ns) const |
Public Attributes | |
address_of_aware_replace_symbolt | replace_const |
bool | is_bottom = true |
Definition at line 78 of file constant_propagator.h.
|
inline |
Definition at line 101 of file constant_propagator.h.
bool constant_propagator_domaint::valuest::is_constant | ( | const exprt & | expr, |
const namespacet & | ns | ||
) | const |
Definition at line 446 of file constant_propagator.cpp.
bool constant_propagator_domaint::valuest::is_constant | ( | const irep_idt & | id, |
const namespacet & | ns | ||
) | const |
Definition at line 453 of file constant_propagator.cpp.
|
inline |
Definition at line 125 of file constant_propagator.h.
|
inline |
Definition at line 106 of file constant_propagator.h.
bool constant_propagator_domaint::valuest::meet | ( | const valuest & | src, |
const namespacet & | ns | ||
) |
meet
Definition at line 606 of file constant_propagator.cpp.
join
Definition at line 535 of file constant_propagator.cpp.
void constant_propagator_domaint::valuest::output | ( | std::ostream & | out, |
const namespacet & | ns | ||
) | const |
Definition at line 498 of file constant_propagator.cpp.
void constant_propagator_domaint::valuest::set_dirty_to_top | ( | const dirtyt & | dirty, |
const namespacet & | ns | ||
) |
Definition at line 473 of file constant_propagator.cpp.
|
inline |
Definition at line 111 of file constant_propagator.h.
|
inline |
Definition at line 89 of file constant_propagator.h.
|
inline |
Definition at line 95 of file constant_propagator.h.
bool constant_propagator_domaint::valuest::set_to_top | ( | const symbol_exprt & | expr | ) |
Do not call this when iterating over replace_const.expr_map!
Definition at line 462 of file constant_propagator.cpp.
Definition at line 82 of file constant_propagator.h.
address_of_aware_replace_symbolt constant_propagator_domaint::valuest::replace_const |
Definition at line 81 of file constant_propagator.h.