cprover
|
Various predicates over pointers in programs. More...
#include "pointer_predicates.h"
#include "arith_tools.h"
#include "c_types.h"
#include "cprover_prefix.h"
#include "namespace.h"
#include "pointer_offset_size.h"
#include "std_expr.h"
#include "symbol.h"
Go to the source code of this file.
Functions | |
exprt | pointer_object (const exprt &p) |
exprt | same_object (const exprt &p1, const exprt &p2) |
exprt | object_size (const exprt &pointer) |
exprt | pointer_offset (const exprt &pointer) |
exprt | malloc_object (const exprt &pointer, const namespacet &ns) |
exprt | deallocated (const exprt &pointer, const namespacet &ns) |
exprt | dead_object (const exprt &pointer, const namespacet &ns) |
exprt | dynamic_size (const namespacet &ns) |
exprt | pointer_object_has_type (const exprt &pointer, const typet &type) |
exprt | dynamic_object (const exprt &pointer) |
exprt | good_pointer (const exprt &pointer) |
exprt | good_pointer_def (const exprt &pointer, const namespacet &ns) |
exprt | null_object (const exprt &pointer) |
exprt | integer_address (const exprt &pointer) |
exprt | null_pointer (const exprt &pointer) |
exprt | invalid_pointer (const exprt &pointer) |
exprt | dynamic_object_lower_bound (const exprt &pointer, const namespacet &ns, const exprt &offset) |
exprt | dynamic_object_upper_bound (const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size) |
exprt | object_upper_bound (const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size) |
exprt | object_lower_bound (const exprt &pointer, const namespacet &ns, const exprt &offset) |
Various predicates over pointers in programs.
Definition in file pointer_predicates.cpp.
exprt dead_object | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 58 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by goto_checkt::pointer_validity_check().
exprt deallocated | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 50 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by value_set_dereferencet::build_reference_to(), good_pointer_def(), and goto_checkt::pointer_validity_check().
Definition at line 76 of file pointer_predicates.cpp.
References exprt::copy_to_operands().
Referenced by 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(), value_sett::guard(), and goto_checkt::pointer_validity_check().
exprt dynamic_object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | ns, | ||
const exprt & | offset | ||
) |
Definition at line 151 of file pointer_predicates.cpp.
References object_lower_bound().
Referenced by value_set_dereferencet::build_reference_to(), good_pointer_def(), and goto_checkt::pointer_validity_check().
exprt dynamic_object_upper_bound | ( | const exprt & | pointer, |
const typet & | dereference_type, | ||
const namespacet & | ns, | ||
const exprt & | access_size | ||
) |
Definition at line 159 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 value_set_dereferencet::build_reference_to(), good_pointer_def(), and goto_checkt::pointer_validity_check().
exprt dynamic_size | ( | const namespacet & | ns | ) |
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 83 of file pointer_predicates.cpp.
exprt good_pointer_def | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 88 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 133 of file pointer_predicates.cpp.
References null_pointer(), same_object(), to_pointer_type(), and exprt::type().
Referenced by mm_io().
Definition at line 146 of file pointer_predicates.cpp.
Referenced by c_typecheck_baset::do_special_functions(), good_pointer_def(), and goto_checkt::pointer_validity_check().
exprt malloc_object | ( | const exprt & | pointer, |
const namespacet & | ns | ||
) |
Definition at line 42 of file pointer_predicates.cpp.
References CPROVER_PREFIX, namespacet::lookup(), same_object(), and symbolt::symbol_expr().
Referenced by goto_checkt::bounds_check(), value_set_dereferencet::build_reference_to(), good_pointer_def(), and goto_checkt::pointer_validity_check().
Definition at line 127 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 140 of file pointer_predicates.cpp.
References null_pointer(), same_object(), to_pointer_type(), and exprt::type().
Referenced by value_set_dereferencet::build_reference_to(), good_pointer_def(), integer_address(), null_object(), null_pointer(), and goto_checkt::pointer_validity_check().
exprt object_lower_bound | ( | const exprt & | pointer, |
const namespacet & | ns, | ||
const exprt & | offset | ||
) |
Definition at line 228 of file pointer_predicates.cpp.
References namespace_baset::follow(), from_integer(), irept::is_not_nil(), pointer_offset(), and exprt::type().
Referenced by dynamic_object_lower_bound(), good_pointer_def(), and goto_checkt::pointer_validity_check().
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 typet & | dereference_type, | ||
const namespacet & | ns, | ||
const exprt & | access_size | ||
) |
Definition at line 193 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 good_pointer_def(), and goto_checkt::pointer_validity_check().
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 71 of file pointer_predicates.cpp.
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().