CBMC
|
This is the complete list of members for abstract_environmentt, including all inherited members.
abstract_environmentt()=delete | abstract_environmentt | |
abstract_environmentt(variable_sensitivity_object_factory_ptrt _object_factory) | abstract_environmentt | inlineexplicit |
abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const | abstract_environmentt | virtual |
abstract_object_factory(const typet &type, const exprt &e, const namespacet &ns) const | abstract_environmentt | virtual |
abstract_object_factory(const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const | abstract_environmentt | private |
assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns) | abstract_environmentt | virtual |
assume(const exprt &expr, const namespacet &ns) | abstract_environmentt | virtual |
bottom | abstract_environmentt | protected |
configuration() const | abstract_environmentt | |
do_assume(const exprt &e, const namespacet &ns) | abstract_environmentt | |
erase(const symbol_exprt &expr) | abstract_environmentt | |
eval(const exprt &expr, const namespacet &ns) const | abstract_environmentt | virtual |
eval_expression(const exprt &e, const namespacet &ns) const | abstract_environmentt | protectedvirtual |
gather_statistics(const namespacet &ns) const | abstract_environmentt | |
havoc(const std::string &havoc_string) | abstract_environmentt | virtual |
is_bottom() const | abstract_environmentt | |
is_top() const | abstract_environmentt | |
make_bottom() | abstract_environmentt | |
make_top() | abstract_environmentt | |
map | abstract_environmentt | protected |
map_keyt typedef | abstract_environmentt | |
merge(const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode) | abstract_environmentt | virtual |
modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second) | abstract_environmentt | static |
object_factory | abstract_environmentt | private |
output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const | abstract_environmentt | |
resolve_symbol(const exprt &e, const namespacet &ns) const | abstract_environmentt | protected |
to_predicate() const | abstract_environmentt | |
verify() const | abstract_environmentt | |
write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write) | abstract_environmentt | virtual |