cprover
|
TO_BE_DOCUMENTED. More...
#include <value_set_dereference.h>
Classes | |
class | valuet |
Public Types | |
enum | modet { modet::READ, modet::WRITE } |
typedef std::unordered_set< exprt, irep_hash > | expr_sett |
Public Member Functions | |
value_set_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode) | |
Constructor. More... | |
virtual | ~value_set_dereferencet () |
virtual exprt | dereference (const exprt &pointer, const guardt &guard, const modet mode) |
Static Public Member Functions | |
static bool | has_dereference (const exprt &expr) |
Returns 'true' iff the given expression contains unary '*'. More... | |
Private Member Functions | |
bool | dereference_type_compare (const typet &object_type, const typet &dereference_type) const |
void | offset_sum (exprt &dest, const exprt &offset) const |
valuet | build_reference_to (const exprt &what, const modet mode, const exprt &pointer, const guardt &guard) |
bool | get_value_guard (const exprt &symbol, const exprt &premise, exprt &value) |
void | bounds_check (const index_exprt &expr, const guardt &guard) |
void | valid_check (const exprt &expr, const guardt &guard, const modet mode) |
void | invalid_pointer (const exprt &expr, const guardt &guard) |
bool | memory_model (exprt &value, const typet &type, const guardt &guard, const exprt &offset) |
bool | memory_model_conversion (exprt &value, const typet &type, const guardt &guard, const exprt &offset) |
bool | memory_model_bytes (exprt &value, const typet &type, const guardt &guard, const exprt &offset) |
Static Private Member Functions | |
static const exprt & | get_symbol (const exprt &object) |
Private Attributes | |
const namespacet & | ns |
symbol_tablet & | new_symbol_table |
const optionst & | options |
dereference_callbackt & | dereference_callback |
const irep_idt | language_mode |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise. More... | |
Static Private Attributes | |
static unsigned | invalid_counter =0 |
TO_BE_DOCUMENTED.
Definition at line 29 of file value_set_dereference.h.
typedef std::unordered_set<exprt, irep_hash> value_set_dereferencet::expr_sett |
Definition at line 79 of file value_set_dereference.h.
|
strong |
Enumerator | |
---|---|
READ | |
WRITE |
Definition at line 54 of file value_set_dereference.h.
|
inline |
Constructor.
_ns | Namespace |
_new_symbol_table | A symbol_table to store new symbols in |
_options | Options, in particular whether pointer checks are to be performed |
_dereference_callback | Callback object for error reporting |
Definition at line 39 of file value_set_dereference.h.
|
inlinevirtual |
Definition at line 52 of file value_set_dereference.h.
|
private |
Definition at line 643 of file value_set_dereference.cpp.
References guardt::add(), index_exprt::array(), array_name(), c_implicit_typecast(), dereference_callback, dereference_callbackt::dereference_failure(), namespace_baset::follow(), from_integer(), optionst::get_bool_option(), irept::id(), index_exprt::index(), irept::is_nil(), exprt::is_zero(), ns, exprt::op0(), options, irept::pretty(), array_typet::size(), to_array_type(), to_integer(), and exprt::type().
Referenced by build_reference_to().
|
private |
Definition at line 274 of file value_set_dereference.cpp.
References guardt::add(), configt::ansi_c, base_type_eq(), bounds_check(), byte_extract_id(), char_type(), config, exprt::copy_to_operands(), CPROVER_PREFIX, deallocated(), dereference_callback, dereference_callbackt::dereference_failure(), dereference_type_compare(), dynamic_object_lower_bound(), dynamic_object_upper_bound(), configt::ansi_ct::endianness, namespace_baset::follow(), from_expr(), from_integer(), from_type(), optionst::get_bool_option(), get_subexpression_at_offset(), irept::id(), irept::id_string(), invalid_pointer(), exprt::is_constant(), exprt::is_zero(), language_mode, binary_relation_exprt::lhs(), namespacet::lookup(), exprt::make_typecast(), malloc_object(), memory_model(), symbolt::name, configt::ansi_ct::NO_ENDIANNESS, ns, null_object(), null_pointer(), object_descriptor_exprt::object(), object_descriptor_exprt::offset(), options, value_set_dereferencet::valuet::pointer_guard, pointer_offset(), pointer_offset_size(), irept::pretty(), binary_relation_exprt::rhs(), object_descriptor_exprt::root_object(), same_object(), size_of_expr(), typet::subtype(), to_object_descriptor_expr(), symbolt::type, exprt::type(), valid_check(), and value_set_dereferencet::valuet::value.
Referenced by dereference().
|
virtual |
The method 'dereference' dereferences the given pointer-expression. Any errors are reported to the callback method given in the constructor.
pointer | A pointer-typed expression, to be dereferenced. |
guard | A guard, which is assumed to hold when dereferencing. |
mode | Indicates whether the dereferencing is a load or store. |
Definition at line 66 of file value_set_dereference.cpp.
References guardt::add(), symbolt::base_name, build_reference_to(), if_exprt::cond(), dereference_callback, if_exprt::false_case(), from_expr(), get_new_name(), dereference_callbackt::get_value_set(), dereference_callbackt::has_failed_symbol(), irept::id(), invalid_counter, invalid_pointer(), symbolt::is_lvalue, irept::is_nil(), symbol_tablet::move(), symbolt::name, new_symbol_table, ns, value_set_dereferencet::valuet::pointer_guard, irept::pretty(), irept::set(), typet::subtype(), symbolt::symbol_expr(), to_if_expr(), if_exprt::true_case(), symbolt::type, exprt::type(), and value_set_dereferencet::valuet::value.
Referenced by goto_program_dereferencet::dereference_rec().
|
private |
Definition at line 215 of file value_set_dereference.cpp.
References base_type_eq(), namespace_baset::follow(), bitvector_typet::get_width(), irept::id(), struct_typet::is_prefix_of(), ns, to_bitvector_type(), and to_struct_type().
Referenced by build_reference_to().
Definition at line 55 of file value_set_dereference.cpp.
References irept::id(), and exprt::op0().
Referenced by valid_check().
|
private |
|
static |
Returns 'true' iff the given expression contains unary '*'.
Definition at line 50 of file value_set_dereference.cpp.
References has_subexpr().
Referenced by goto_program_dereferencet::dereference_rec(), and rw_range_set_value_sett::get_objects_dereference().
Definition at line 257 of file value_set_dereference.cpp.
References guardt::add(), dereference_callback, dereference_callbackt::dereference_failure(), optionst::get_bool_option(), and options.
Referenced by build_reference_to(), and dereference().
|
private |
Definition at line 740 of file value_set_dereference.cpp.
References bv_width(), from_type(), irept::id(), is_a_bv_type(), memory_model_bytes(), memory_model_conversion(), ns, and exprt::type().
Referenced by build_reference_to().
|
private |
Definition at line 812 of file value_set_dereference.cpp.
References guardt::add(), configt::ansi_c, base_type_eq(), byte_extract_id(), config, exprt::copy_to_operands(), dereference_callback, dereference_callbackt::dereference_failure(), configt::ansi_ct::endianness, namespace_baset::follow(), from_integer(), from_type(), optionst::get_bool_option(), irept::id(), INVARIANT, is_a_bv_type(), irept::is_not_nil(), exprt::is_zero(), exprt::make_typecast(), configt::ansi_ct::NO_ENDIANNESS, ns, options, pointer_offset_size(), irept::pretty(), size_of_expr(), size_type(), typet::subtype(), and exprt::type().
Referenced by memory_model().
|
private |
Definition at line 785 of file value_set_dereference.cpp.
References guardt::add(), dereference_callback, dereference_callbackt::dereference_failure(), from_integer(), optionst::get_bool_option(), exprt::make_not(), exprt::make_typecast(), options, and exprt::type().
Referenced by memory_model().
|
private |
Definition at line 591 of file value_set_dereference.cpp.
References dereference_callback, dereference_callbackt::dereference_failure(), irept::get_bool(), optionst::get_bool_option(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), get_symbol(), irept::id(), irept::is_nil(), is_ssa_expr(), namespacet::lookup(), ns, options, to_ssa_expr(), to_symbol_expr(), symbolt::type, and WRITE.
Referenced by build_reference_to().
|
private |
Definition at line 85 of file value_set_dereference.h.
Referenced by bounds_check(), build_reference_to(), dereference(), invalid_pointer(), memory_model_bytes(), memory_model_conversion(), and valid_check().
|
staticprivate |
Definition at line 89 of file value_set_dereference.h.
Referenced by dereference().
|
private |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
Definition at line 88 of file value_set_dereference.h.
Referenced by build_reference_to().
|
private |
Definition at line 83 of file value_set_dereference.h.
Referenced by dereference().
|
private |
Definition at line 82 of file value_set_dereference.h.
Referenced by bounds_check(), build_reference_to(), dereference(), dereference_type_compare(), memory_model(), memory_model_bytes(), and valid_check().
|
private |
Definition at line 84 of file value_set_dereference.h.
Referenced by bounds_check(), build_reference_to(), invalid_pointer(), memory_model_bytes(), memory_model_conversion(), and valid_check().