CBMC
gdb_value_extractort::memory_scopet Struct Reference
+ Collaboration diagram for gdb_value_extractort::memory_scopet:

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. More...
 
mp_integer distance (const memory_addresst &point, mp_integer member_size) const
 Compute the distance of point from the beginning of this scope. More...
 
irep_idt id () const
 Getter for the name of this memory scope. More...
 
mp_integer size () const
 Getter for the allocation size of this memory scope. More...
 

Private Member Functions

size_t address2size_t (const memory_addresst &point) const
 Convert base-16 memory address to a natural number. More...
 
bool check_containment (const size_t &point_int) const
 Helper function that check if a point in memory points inside this scope. More...
 

Private Attributes

size_t begin_int
 
mp_integer byte_size
 
irep_idt name
 

Detailed Description

Definition at line 94 of file analyze_symbol.h.

Constructor & Destructor Documentation

◆ memory_scopet()

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.

Member Function Documentation

◆ address2size_t()

size_t gdb_value_extractort::memory_scopet::address2size_t ( const memory_addresst point) const
private

Convert base-16 memory address to a natural number.

Parameters
pointthe memory address to be converted
Returns
base-10 unsigned integer equal in value to point

Definition at line 45 of file analyze_symbol.cpp.

◆ check_containment()

bool gdb_value_extractort::memory_scopet::check_containment ( const size_t &  point_int) const
inlineprivate

Helper function that check if a point in memory points inside this scope.

Parameters
point_intmemory point as natural number
Returns
true if the point is inside this scope

Definition at line 109 of file analyze_symbol.h.

◆ contains()

bool gdb_value_extractort::memory_scopet::contains ( const memory_addresst point) const
inline

Check if point points somewhere in this memory scope.

Parameters
pointmemory address to be check for presence
Returns
true if point is inside *this

Definition at line 123 of file analyze_symbol.h.

◆ distance()

mp_integer gdb_value_extractort::memory_scopet::distance ( const memory_addresst point,
mp_integer  member_size 
) const

Compute the distance of point from the beginning of this scope.

Parameters
pointmemory address to have the offset computed
member_sizesize of one element of this scope in bytes
Returns
‘n’ such that point is the n-th element of this scope

Definition at line 51 of file analyze_symbol.cpp.

◆ id()

irep_idt gdb_value_extractort::memory_scopet::id ( ) const
inline

Getter for the name of this memory scope.

Returns
the name as irep id

Definition at line 137 of file analyze_symbol.h.

◆ size()

mp_integer gdb_value_extractort::memory_scopet::size ( ) const
inline

Getter for the allocation size of this memory scope.

Returns
the size in bytes

Definition at line 144 of file analyze_symbol.h.

Member Data Documentation

◆ begin_int

size_t gdb_value_extractort::memory_scopet::begin_int
private

Definition at line 97 of file analyze_symbol.h.

◆ byte_size

mp_integer gdb_value_extractort::memory_scopet::byte_size
private

Definition at line 98 of file analyze_symbol.h.

◆ name

irep_idt gdb_value_extractort::memory_scopet::name
private

Definition at line 99 of file analyze_symbol.h.


The documentation for this struct was generated from the following files: