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...
|
|
Wrapper for a function dereferencing pointer expressions using a value set.
Definition at line 27 of file value_set_dereference.h.
◆ modet
◆ 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 given dereference may follow a null pointer |
Definition at line 38 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 |
- Returns
- a
valuet
object containing guard
, value
and ignore
fields. The ignore
field is true for a null
object when exclude_null_derefs
is true and integer addresses in java mode. The guard is an appropriate check to determine whether pointer_expr
really points to 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), .ignore = false}
Definition at line 271 of file value_set_dereference.cpp.
◆ dereference()
exprt value_set_dereferencet::dereference |
( |
const exprt & |
pointer, |
|
|
const guardt & |
guard, |
|
|
const modet |
mode |
|
) |
| |
|
virtual |
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. |
guard | A guard, which is assumed to hold when dereferencing. |
mode | Indicates whether the dereferencing is a load or store (unused). |
Definition at line 35 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 |
|
private |
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 193 of file value_set_dereference.cpp.
◆ memory_model()
bool value_set_dereferencet::memory_model |
( |
exprt & |
value, |
|
|
const typet & |
to_type, |
|
|
const exprt & |
offset |
|
) |
| |
|
private |
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 521 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 |
|
) |
| |
|
private |
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 567 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 |
language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
Definition at line 74 of file value_set_dereference.h.
◆ new_symbol_table
◆ ns
The documentation for this class was generated from the following files: