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

#include <pointer_logic.h>

+ Collaboration diagram for pointer_logict:

Classes

struct  pointert
 

Public Member Functions

exprt pointer_expr (const pointert &pointer, const pointer_typet &type) const
 Convert an (object,offset) pair to an expression. More...
 
exprt pointer_expr (const mp_integer &object, const pointer_typet &type) const
 Convert an (object,0) pair to an expression. More...
 
 ~pointer_logict ()
 
 pointer_logict (const namespacet &_ns)
 
mp_integer add_object (const exprt &expr)
 
const mp_integer & get_null_object () const
 
const mp_integer & get_invalid_object () const
 
bool is_dynamic_object (const exprt &expr) const
 
void get_dynamic_objects (std::vector< mp_integer > &objects) const
 

Public Attributes

numberingt< exprt, irep_hash > objects
 

Protected Attributes

const namespacet & ns
 
mp_integer null_object
 
mp_integer invalid_object
 

Detailed Description

Definition at line 22 of file pointer_logic.h.

Constructor & Destructor Documentation

◆ ~pointer_logict()

pointer_logict::~pointer_logict ( )

Definition at line 169 of file pointer_logic.cpp.

◆ pointer_logict()

pointer_logict::pointer_logict ( const namespacet &  _ns)
explicit

Definition at line 159 of file pointer_logic.cpp.

Member Function Documentation

◆ add_object()

mp_integer pointer_logict::add_object ( const exprt &  expr)

Definition at line 44 of file pointer_logic.cpp.

◆ get_dynamic_objects()

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

Definition at line 34 of file pointer_logic.cpp.

◆ get_invalid_object()

const mp_integer& pointer_logict::get_invalid_object ( ) const
inline
Returns
number of INVALID object

Definition at line 58 of file pointer_logic.h.

◆ get_null_object()

const mp_integer& pointer_logict::get_null_object ( ) const
inline
Returns
number of NULL object

Definition at line 52 of file pointer_logic.h.

◆ is_dynamic_object()

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

Definition at line 25 of file pointer_logic.cpp.

◆ pointer_expr() [1/2]

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

Convert an (object,0) pair to an expression.

Definition at line 60 of file pointer_logic.cpp.

◆ pointer_expr() [2/2]

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

Convert an (object,offset) pair to an expression.

Definition at line 67 of file pointer_logic.cpp.

Member Data Documentation

◆ invalid_object

mp_integer pointer_logict::invalid_object
protected

Definition at line 69 of file pointer_logic.h.

◆ ns

const namespacet& pointer_logict::ns
protected

Definition at line 68 of file pointer_logic.h.

◆ null_object

mp_integer pointer_logict::null_object
protected

Definition at line 69 of file pointer_logic.h.

◆ objects

numberingt<exprt, irep_hash> pointer_logict::objects

Definition at line 26 of file pointer_logic.h.

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