cprover
Classes | Public Types | Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
pointer_logict Class Reference

#include <pointer_logic.h>

+ Collaboration diagram for pointer_logict:

Classes

struct  pointert
 

Public Types

typedef hash_numbering< exprt, irep_hash > objectst
 

Public Member Functions

exprt pointer_expr (const pointert &pointer, const pointer_typet &type) const
 
exprt pointer_expr (std::size_t object, const pointer_typet &type) const
 
 ~pointer_logict ()
 
 pointer_logict (const namespacet &_ns)
 
std::size_t add_object (const exprt &expr)
 
std::size_t get_null_object () const
 
std::size_t get_invalid_object () const
 
bool is_dynamic_object (const exprt &expr) const
 
void get_dynamic_objects (std::vector< std::size_t > &objects) const
 

Public Attributes

objectst objects
 

Protected Member Functions

exprt pointer_expr (const mp_integer &offset, const exprt &object) const
 

Protected Attributes

const namespacet & ns
 
std::size_t null_object
 
std::size_t invalid_object
 

Detailed Description

Definition at line 22 of file pointer_logic.h.

Member Typedef Documentation

◆ objectst

typedef hash_numbering<exprt, irep_hash> pointer_logict::objectst

Definition at line 26 of file pointer_logic.h.

Constructor & Destructor Documentation

◆ ~pointer_logict()

pointer_logict::~pointer_logict ( )

Definition at line 155 of file pointer_logic.cpp.

◆ pointer_logict()

pointer_logict::pointer_logict ( const namespacet &  _ns)
explicit

Definition at line 145 of file pointer_logic.cpp.

Member Function Documentation

◆ add_object()

std::size_t pointer_logict::add_object ( const exprt &  expr)

Definition at line 49 of file pointer_logic.cpp.

◆ get_dynamic_objects()

void pointer_logict::get_dynamic_objects ( std::vector< std::size_t > &  objects) const

Definition at line 36 of file pointer_logic.cpp.

◆ get_invalid_object()

std::size_t pointer_logict::get_invalid_object ( ) const
inline

Definition at line 65 of file pointer_logic.h.

◆ get_null_object()

std::size_t pointer_logict::get_null_object ( ) const
inline

Definition at line 59 of file pointer_logic.h.

◆ is_dynamic_object()

bool pointer_logict::is_dynamic_object ( const exprt &  expr) const

Definition at line 23 of file pointer_logic.cpp.

◆ pointer_expr() [1/3]

exprt pointer_logict::pointer_expr ( const pointert &  pointer,
const pointer_typet &  type 
) const

Definition at line 73 of file pointer_logic.cpp.

◆ pointer_expr() [2/3]

exprt pointer_logict::pointer_expr ( std::size_t  object,
const pointer_typet &  type 
) const

Definition at line 65 of file pointer_logic.cpp.

◆ pointer_expr() [3/3]

exprt pointer_logict::pointer_expr ( const mp_integer &  offset,
const exprt &  object 
) const
protected

Member Data Documentation

◆ invalid_object

std::size_t pointer_logict::invalid_object
protected

Definition at line 76 of file pointer_logic.h.

◆ ns

const namespacet& pointer_logict::ns
protected

Definition at line 75 of file pointer_logic.h.

◆ null_object

std::size_t pointer_logict::null_object
protected

Definition at line 76 of file pointer_logic.h.

◆ objects

objectst pointer_logict::objects

Definition at line 27 of file pointer_logic.h.

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