cprover
|
Various predicates over pointers in programs. More...
Go to the source code of this file.
Various predicates over pointers in programs.
Definition in file pointer_predicates.h.
exprt dead_object | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 58 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by goto_checkt::address_check().
exprt deallocated | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 50 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by goto_checkt::address_check(), value_set_dereferencet::build_reference_to(), and good_pointer_def().
Definition at line 71 of file pointer_predicates.cpp.
References exprt::copy_to_operands().
Referenced by goto_checkt::address_check(), allocate_dynamic_object_with_decl(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), goto_checkt::bounds_check(), value_set_dereferencet::build_reference_to(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::do_free(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), good_pointer_def(), and value_sett::guard().
exprt dynamic_object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | offset | ||
) |
Definition at line 146 of file pointer_predicates.cpp.
References object_lower_bound().
Referenced by goto_checkt::address_check(), value_set_dereferencet::build_reference_to(), and good_pointer_def().
exprt dynamic_object_upper_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | access_size | ||
) |
Definition at line 154 of file pointer_predicates.cpp.
References dynamic_size(), namespace_baset::follow(), irept::is_not_nil(), exprt::make_typecast(), pointer_offset(), and exprt::type().
Referenced by goto_checkt::address_check(), value_set_dereferencet::build_reference_to(), and good_pointer_def().
exprt dynamic_size | ( | const namespacet & | ) |
Definition at line 66 of file pointer_predicates.cpp.
References CPROVER_PREFIX, and namespacet::lookup().
Referenced by goto_checkt::bounds_check(), and dynamic_object_upper_bound().
Definition at line 78 of file pointer_predicates.cpp.
exprt good_pointer_def | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 83 of file pointer_predicates.cpp.
References deallocated(), dynamic_object(), dynamic_object_lower_bound(), dynamic_object_upper_bound(), namespace_baset::follow(), invalid_pointer(), malloc_object(), null_pointer(), object_lower_bound(), object_upper_bound(), pointer_type(), size_of_expr(), typet::subtype(), to_pointer_type(), and exprt::type().
Referenced by simplify_exprt::simplify_good_pointer().
Definition at line 128 of file pointer_predicates.cpp.
References null_pointer(), same_object(), to_pointer_type(), and exprt::type().
Referenced by goto_checkt::address_check(), and mm_io().
Definition at line 141 of file pointer_predicates.cpp.
Referenced by goto_checkt::address_check(), c_typecheck_baset::do_special_functions(), and good_pointer_def().
exprt malloc_object | ( | const exprt & | pointer, |
const namespacet & | |||
) |
Definition at line 42 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by goto_checkt::address_check(), goto_checkt::bounds_check(), value_set_dereferencet::build_reference_to(), and good_pointer_def().
Definition at line 122 of file pointer_predicates.cpp.
References null_pointer(), same_object(), to_pointer_type(), and exprt::type().
Referenced by value_set_dereferencet::build_reference_to().
Definition at line 135 of file pointer_predicates.cpp.
References null_pointer(), same_object(), to_pointer_type(), and exprt::type().
Referenced by goto_checkt::address_check(), value_set_dereferencet::build_reference_to(), good_pointer_def(), integer_address(), null_object(), and null_pointer().
exprt object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | offset | ||
) |
Definition at line 221 of file pointer_predicates.cpp.
References namespace_baset::follow(), from_integer(), irept::is_not_nil(), pointer_offset(), and exprt::type().
Referenced by goto_checkt::address_check(), dynamic_object_lower_bound(), and good_pointer_def().
Definition at line 32 of file pointer_predicates.cpp.
References size_type().
Referenced by allocate_dynamic_object(), goto_checkt::bounds_check(), smt2_convt::define_object_size(), goto_convertt::do_cpp_new(), bv_pointerst::do_postponed(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), and object_upper_bound().
exprt object_upper_bound | ( | const exprt & | pointer, |
const namespacet & | , | ||
const exprt & | access_size | ||
) |
Definition at line 187 of file pointer_predicates.cpp.
References namespace_baset::follow(), irept::is_not_nil(), exprt::make_typecast(), object_size(), pointer_offset(), and exprt::type().
Referenced by goto_checkt::address_check(), and good_pointer_def().
Definition at line 22 of file pointer_predicates.cpp.
References size_type().
Referenced by c_typecheck_baset::do_special_functions(), and same_object().
Definition at line 37 of file pointer_predicates.cpp.
References signed_size_type().
Referenced by goto_checkt::bounds_check(), string_abstractiont::build(), value_set_dereferencet::build_reference_to(), c_typecheck_baset::do_special_functions(), dynamic_object_upper_bound(), object_lower_bound(), object_upper_bound(), and simplify_exprt::simplify_pointer_offset().
Definition at line 27 of file pointer_predicates.cpp.
References pointer_object().
Referenced by value_set_dereferencet::build_reference_to(), dead_object(), deallocated(), c_typecheck_baset::do_special_functions(), integer_address(), malloc_object(), null_object(), null_pointer(), and goto_checkt::pointer_rel_check().