|
cprover
|
Public Member Functions | |
| memory_scopet (const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name) | |
| bool | contains (const memory_addresst &point) const |
Check if point points somewhere in this memory scope. | |
| irep_idt | id () const |
Compute the distance of point from the beginning of this scope. | |
| mp_integer | size () const |
| Getter for the allocation size of this memory scope. | |
Private Member Functions | |
| size_t | address2size_t (const memory_addresst &point) const |
| Convert base-16 memory address to a natural number. | |
| bool | check_containment (const size_t &point_int) const |
| Helper function that check if a point in memory points inside this scope. | |
Private Attributes | |
| size_t | begin_int |
| mp_integer | byte_size |
| irep_idt | name |
Definition at line 94 of file analyze_symbol.h.
| gdb_value_extractort::memory_scopet::memory_scopet | ( | const memory_addresst & | begin, |
| const mp_integer & | byte_size, | ||
| const irep_idt & | name ) |
Definition at line 35 of file analyze_symbol.cpp.
|
private |
Convert base-16 memory address to a natural number.
| point | the memory address to be converted |
point Definition at line 45 of file analyze_symbol.cpp.
|
inlineprivate |
Helper function that check if a point in memory points inside this scope.
| point_int | memory point as natural number |
Definition at line 109 of file analyze_symbol.h.
|
inline |
Check if point points somewhere in this memory scope.
| point | memory address to be check for presence |
point is inside *this Definition at line 123 of file analyze_symbol.h.
|
inline |
Compute the distance of point from the beginning of this scope.
| point | memory address to have the offset computed |
| member_size | size of one element of this scope in bytes |
point is the n-th element of this scope */ mp_integer distance(const memory_addresst &point, mp_integer member_size) const;/** Getter for the name of this memory scope
Definition at line 137 of file analyze_symbol.h.
|
inline |
Getter for the allocation size of this memory scope.
Definition at line 144 of file analyze_symbol.h.
|
private |
Definition at line 97 of file analyze_symbol.h.
|
private |
Definition at line 98 of file analyze_symbol.h.
|
private |
Definition at line 99 of file analyze_symbol.h.