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 typet &type) const
 
exprt pointer_expr (std::size_t object, const 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 23 of file pointer_logic.h.

Member Typedef Documentation

§ objectst

Constructor & Destructor Documentation

§ ~pointer_logict()

pointer_logict::~pointer_logict ( )

Definition at line 206 of file pointer_logic.cpp.

Referenced by pointer_logict::pointert::pointert().

§ pointer_logict()

pointer_logict::pointer_logict ( const namespacet _ns)
explicit

Member Function Documentation

§ add_object()

§ 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

§ get_null_object()

§ 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 typet type 
) const

Definition at line 66 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 77 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 76 of file pointer_logic.h.

Referenced by object_rec().

§ null_object

std::size_t pointer_logict::null_object
protected

Definition at line 77 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: