cprover
|
TO_BE_DOCUMENTED. More...
#include <value_set_dereference.h>
Classes | |
class | valuet |
Return value for build_reference_to ; see that method for documentation. More... | |
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, bool _exclude_null_derefs) | |
Constructor. More... | |
virtual | ~value_set_dereferencet () |
virtual exprt | dereference (const exprt &pointer, const guardt &guard, const modet mode) |
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) |
Get a guard and expression to access what under guard . More... | |
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... | |
const bool | exclude_null_derefs |
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to dereference NULL. 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 81 of file value_set_dereference.h.
|
strong |
Enumerator | |
---|---|
READ | |
WRITE |
Definition at line 60 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 |
_language_mode | Mode for any new symbols created to represent a dereference failure |
_exclude_null_derefs | Ignore value-set entries that indicate a given dereference may follow a null pointer |
Definition at line 43 of file value_set_dereference.h.
|
inlinevirtual |
Definition at line 58 of file value_set_dereference.h.
|
private |
Definition at line 663 of file value_set_dereference.cpp.
References guardt::add(), index_exprt::array(), array_name(), typecast_exprt::conditional_cast(), 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 |
Get a guard and expression to access what
under guard
.
what | value set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset. |
mode | whether the pointer is being read or written; used to create pointer validity checks if need be |
pointer | pointer expression that may point to what |
guard | guard under which the pointer is dereferenced |
what
as a possible pointer target: a valuet
with ignore
= true, and value
and pointer_guard
set to nil.what
: A valuet
with non-nil value
, and pointer_guard
set to an appropriate check to determine if pointer_expr
really points to what
(for example, we might return {.value = global, .pointer_guard = (pointer_expr == &global)}
what
== ID_unknown), a valuet
with nil value
and ignore
== false. Definition at line 288 of file value_set_dereference.cpp.
References guardt::add(), configt::ansi_c, base_type_eq(), bounds_check(), byte_extract_id(), config, CPROVER_PREFIX, deallocated(), dereference_callback, dereference_callbackt::dereference_failure(), dereference_type_compare(), dynamic_object(), dynamic_object_lower_bound(), dynamic_object_upper_bound(), configt::ansi_ct::endianness, exclude_null_derefs, namespace_baset::follow(), format(), from_integer(), optionst::get_bool_option(), get_subexpression_at_offset(), irept::id(), irept::id_string(), value_set_dereferencet::valuet::ignore, 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 48 of file value_set_dereference.cpp.
References guardt::add(), build_reference_to(), if_exprt::cond(), dereference_callback, if_exprt::false_case(), format(), get_fresh_aux_symbol(), dereference_callbackt::get_value_set(), dereference_callbackt::has_failed_symbol(), irept::id(), value_set_dereferencet::valuet::ignore, invalid_pointer(), symbolt::is_lvalue, irept::is_nil(), language_mode, new_symbol_table, value_set_dereferencet::valuet::pointer_guard, irept::pretty(), irept::set(), exprt::source_location(), typet::subtype(), symbolt::symbol_expr(), to_if_expr(), if_exprt::true_case(), exprt::type(), and value_set_dereferencet::valuet::value.
Referenced by goto_program_dereferencet::dereference_rec().
|
private |
Definition at line 199 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, irept::pretty(), typet::subtype(), to_bitvector_type(), and to_struct_type().
Referenced by build_reference_to().
Definition at line 37 of file value_set_dereference.cpp.
References irept::id(), and exprt::op0().
Referenced by valid_check().
|
private |
Definition at line 271 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 743 of file value_set_dereference.cpp.
References from_type(), irept::id(), is_a_bv_type(), memory_model_bytes(), memory_model_conversion(), ns, pointer_offset_bits(), and exprt::type().
Referenced by build_reference_to().
|
private |
Definition at line 815 of file value_set_dereference.cpp.
References guardt::add(), configt::ansi_c, base_type_eq(), byte_extract_id(), config, 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 788 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 611 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 87 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().
|
private |
Flag indicating whether value_set_dereferencet::dereference
should disregard an apparent attempt to dereference NULL.
Definition at line 93 of file value_set_dereference.h.
Referenced by build_reference_to().
|
staticprivate |
Definition at line 94 of file value_set_dereference.h.
|
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 90 of file value_set_dereference.h.
Referenced by build_reference_to(), and dereference().
|
private |
Definition at line 85 of file value_set_dereference.h.
Referenced by dereference().
|
private |
Definition at line 84 of file value_set_dereference.h.
Referenced by bounds_check(), build_reference_to(), dereference_type_compare(), memory_model(), memory_model_bytes(), and valid_check().
|
private |
Definition at line 86 of file value_set_dereference.h.
Referenced by bounds_check(), build_reference_to(), invalid_pointer(), memory_model_bytes(), memory_model_conversion(), and valid_check().