CBMC: Member List

abstract_object_meet(const abstract_object_pointert &other) const abstract_objectt protected

abstract_object_meet_internal(const abstract_object_pointert &other) const abstract_objectt privatevirtual

abstract_object_merge(const abstract_object_pointert &other) const abstract_objectt protected

abstract_object_merge_internal(const abstract_object_pointert &other) const abstract_objectt privatevirtual

abstract_objectt(const typet &type, bool top, bool bottom) abstract_objectt

abstract_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) abstract_objectt

abstract_pointer_objectt(const typet &type, bool top, bool bottom) abstract_pointer_objectt

abstract_pointer_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) abstract_pointer_objectt explicit

bottom abstract_objectt private

clear_top() const abstract_objectt inline

dump_map(std::ostream out, const shared_mapt &m) abstract_objectt static

dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2) abstract_objectt static

eval_ptr_comparison(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const abstract_pointer_objectt private

eval_ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const abstract_pointer_objectt private

expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override abstract_pointer_objectt virtual

get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override abstract_pointer_objectt virtual

has_been_modified(const abstract_object_pointert &before) const abstract_objectt inlinevirtual

internal_abstract_object_pointert typedef abstract_objectt protected

internal_equality(const abstract_object_pointert &other) const abstract_objectt inlinevirtual

internal_hash() const abstract_objectt inlinevirtual

internal_sharing_ptrt typedef abstract_objectt protected

is_bottom() const abstract_objectt virtual

is_top() const abstract_objectt virtual

locationt typedef abstract_objectt

make_top() const abstract_objectt inline

meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2) abstract_objectt static

meet(const abstract_object_pointert &other) const abstract_objectt virtual

merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode) abstract_objectt static

merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode) abstract_objectt static

merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const abstract_objectt protectedvirtual

merge_location_context(const locationt &location) const abstract_objectt virtual

mutable_clone() const abstract_objectt inlineprotectedvirtual

output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const abstract_objectt virtual

ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0 abstract_pointer_objectt pure virtual

ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const =0 abstract_pointer_objectt pure virtual

read_dereference(const abstract_environmentt &env, const namespacet &ns) const =0 abstract_pointer_objectt pure virtual

set_not_bottom() abstract_objectt inlineprotected

set_not_top() abstract_objectt inlineprotected

set_not_top_internal() abstract_objectt inlineprivatevirtual

set_top() abstract_objectt inlineprotected

set_top_internal() abstract_objectt inlineprivatevirtual

shared_mapt typedef abstract_objectt

should_use_base_meet(const abstract_object_pointert &other) const abstract_objectt protected

should_use_base_merge(const abstract_object_pointert &other) const abstract_objectt protected

t abstract_objectt private

to_constant() const abstract_objectt virtual

to_predicate(const exprt &name) const abstract_objectt

to_predicate_internal(const exprt &name) const abstract_objectt virtual

top abstract_objectt private

type() const abstract_objectt virtual

typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const =0 abstract_pointer_objectt pure virtual

typecast_from_void_ptr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const abstract_pointer_objectt private

unwrap_context() const abstract_objectt virtual

verify() const abstract_objectt virtual

visit_sub_elements(const abstract_object_visitort &visitor) const abstract_objectt inlinevirtual

write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override abstract_pointer_objectt virtual

write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const =0 abstract_pointer_objectt pure virtual

write_location_context(const locationt &location) const abstract_objectt virtual

~abstract_objectt() abstract_objectt inlinevirtual