Wrapper for a function dereferencing pointer expressions using a value set.
More...
#include <value_set_dereference.h>
|
| class | valuet |
| | Return value for build_reference_to; see that method for documentation. More...
|
| |
|
| static bool | should_ignore_value (const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode) |
| | Determine whether possible alias what should be ignored when replacing a pointer by its referees. More...
|
| |
| static valuet | build_reference_to (const exprt &what, const exprt &pointer, const namespacet &ns) |
| |
| static bool | dereference_type_compare (const typet &object_type, const typet &dereference_type, const namespacet &ns) |
| | Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example: More...
|
| |
| static bool | memory_model (exprt &value, const typet &type, const exprt &offset, const namespacet &ns) |
| | Replace value by an expression of type to_type corresponding to the value at memory address value + offset. More...
|
| |
| static bool | memory_model_bytes (exprt &value, const typet &type, const exprt &offset, const namespacet &ns) |
| | Replace value by an expression of type to_type corresponding to the value at memory address value + offset. More...
|
| |
Wrapper for a function dereferencing pointer expressions using a value set.
Definition at line 22 of file value_set_dereference.h.
◆ value_set_dereferencet()
- Parameters
-
| _ns | Namespace |
| _new_symbol_table | A symbol_table to store new symbols in |
| _dereference_callback | Callback object for getting the set of objects a given pointer may point to. |
| _language_mode | Mode for any new symbols created to represent a dereference failure |
| _exclude_null_derefs | Ignore value-set entries that indicate a |
| _log | Messaget object for displaying points-to set |
Definition at line 34 of file value_set_dereference.h.
◆ ~value_set_dereferencet()
| virtual value_set_dereferencet::~value_set_dereferencet |
( |
| ) |
|
|
inlinevirtual |
◆ build_reference_to()
- Parameters
-
| 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. |
| pointer_expr | pointer expression that may point to what |
| ns | A namespace |
- Returns
- a
valuet object containing guard and value fields. The guard is an appropriate check to determine whether pointer_expr really points to what; for example pointer_expr == &what. The value corresponds to the dereferenced pointer_expr assuming it is pointing to the object described by what. For example, we might return {.value = global, .pointer_guard = (pointer_expr == &global)}
Definition at line 453 of file value_set_dereference.cpp.
◆ dereference()
| exprt value_set_dereferencet::dereference |
( |
const exprt & |
pointer, |
|
|
bool |
display_points_to_sets = false |
|
) |
| |
Dereference the given pointer-expression.
Any errors are reported to the callback method given in the constructor.
- Parameters
-
| pointer | A pointer-typed expression, to be dereferenced. |
| display_points_to_sets | Display size and contents of points to sets |
Definition at line 141 of file value_set_dereference.cpp.
◆ dereference_type_compare()
| bool value_set_dereferencet::dereference_type_compare |
( |
const typet & |
object_type, |
|
|
const typet & |
dereference_type, |
|
|
const namespacet & |
ns |
|
) |
| |
|
static |
Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example:
- dereference_type=void is ok (no matter what object_type is);
- object_type=(int *), dereference_type=(void *) is ok;
- object_type=(int **), dereference_type=(void **) is ok;
- object_type=(int **), dereference_type=(void *) is ok;
- object_type=(int *), dereference_type=(void **) is not ok;
Definition at line 337 of file value_set_dereference.cpp.
◆ get_failure_value()
◆ handle_dereference_base_case()
| exprt value_set_dereferencet::handle_dereference_base_case |
( |
const exprt & |
pointer, |
|
|
bool |
display_points_to_sets |
|
) |
| |
|
private |
◆ memory_model()
| bool value_set_dereferencet::memory_model |
( |
exprt & |
value, |
|
|
const typet & |
to_type, |
|
|
const exprt & |
offset, |
|
|
const namespacet & |
ns |
|
) |
| |
|
static |
Replace value by an expression of type to_type corresponding to the value at memory address value + offset.
If value is a bitvector or pointer of the same size as to_type, make value into the typecast expression (to_type)value. Otherwise perform the same operation as value_set_dereferencet::memory_model_bytes
- Returns
- true on success
Definition at line 683 of file value_set_dereference.cpp.
◆ memory_model_bytes()
| bool value_set_dereferencet::memory_model_bytes |
( |
exprt & |
value, |
|
|
const typet & |
to_type, |
|
|
const exprt & |
offset, |
|
|
const namespacet & |
ns |
|
) |
| |
|
static |
Replace value by an expression of type to_type corresponding to the value at memory address value + offset.
If the type of value is an array of bitvectors of size 1 byte, and to_type also is bitvector of size 1 byte, then the resulting expression is value[offset] or (to_type)value[offset] when typecast is required. Otherwise the expression is byte_extract(value, offset).
- Returns
- false if the conversion cannot be made
Definition at line 730 of file value_set_dereference.cpp.
◆ should_ignore_value()
| bool value_set_dereferencet::should_ignore_value |
( |
const exprt & |
what, |
|
|
bool |
exclude_null_derefs, |
|
|
const irep_idt & |
language_mode |
|
) |
| |
|
static |
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
We currently ignore a null object when exclude_null_derefs is true (pass true if you know the dereferenced pointer cannot be null), and also ignore integer addresses when language_mode is "java"
- Parameters
-
| 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. |
| exclude_null_derefs | Ignore value-set entries that indicate a given dereference may follow a null pointer |
| language_mode | Mode for any new symbols created to represent a dereference failure |
- Returns
- true if
what should be ignored as a possible alias
Definition at line 416 of file value_set_dereference.cpp.
◆ dereference_callback
◆ exclude_null_derefs
| const bool value_set_dereferencet::exclude_null_derefs |
|
private |
◆ language_mode
| const irep_idt value_set_dereferencet::language_mode |
|
private |
◆ log
| const messaget& value_set_dereferencet::log |
|
private |
◆ new_symbol_table
◆ ns
The documentation for this class was generated from the following files:
Collaboration diagram for value_set_dereferencet: