cprover
pointer_logict Class Reference

#include <pointer_logic.h>

Collaboration diagram for pointer_logict:
[legend]

Classes

struct  pointert
 

Public Types

typedef hash_numbering< exprt, irep_hashobjectst
 

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
 
exprt object_rec (const mp_integer &offset, const typet &pointer_type, const exprt &src) const
 

Protected Attributes

const namespacetns
 
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

Constructor & Destructor Documentation

◆ ~pointer_logict()

pointer_logict::~pointer_logict ( )

Definition at line 192 of file pointer_logic.cpp.

◆ pointer_logict()

pointer_logict::pointer_logict ( const namespacet _ns)
explicit

Member Function Documentation

◆ add_object()

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

◆ get_dynamic_objects()

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

◆ get_invalid_object()

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

Definition at line 65 of file pointer_logic.h.

References invalid_object.

Referenced by smt2_convt::convert_expr(), and bv_pointerst::convert_rest().

◆ get_null_object()

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

◆ is_dynamic_object()

bool pointer_logict::is_dynamic_object ( const exprt expr) const

◆ object_rec()

exprt pointer_logict::object_rec ( const mp_integer offset,
const typet pointer_type,
const exprt src 
) const
protected

◆ pointer_expr() [1/3]

◆ pointer_expr() [2/3]

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

Definition at line 67 of file pointer_logic.cpp.

References pointer_expr().

◆ 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.

Referenced by get_invalid_object(), pointer_expr(), and pointer_logict().

◆ ns

const namespacet& pointer_logict::ns
protected

Definition at line 75 of file pointer_logic.h.

Referenced by object_rec().

◆ null_object

std::size_t pointer_logict::null_object
protected

Definition at line 76 of file pointer_logic.h.

Referenced by get_null_object(), pointer_expr(), and pointer_logict().

◆ objects


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