pointer_logict Class Reference

#include <pointer_logic.h>

Classes
struct	pointert

Public Types
typedef std::unordered_map< expr2tc, unsigned int, irep2_hash >	objectst
typedef std::vector< expr2tc >	obj_lookupt

Public Member Functions
expr2tc	pointer_expr (const pointert &pointer, const type2tc &type) const
expr2tc	pointer_expr (unsigned object, const type2tc &type) const
	~pointer_logict ()=default
	pointer_logict ()
unsigned	add_object (const expr2tc &expr)
unsigned	get_null_object () const
unsigned	get_invalid_object () const
unsigned	get_free_obj_num ()

Public Attributes
objectst	objects
obj_lookupt	lookup
unsigned int	obj_num_offset

Protected Member Functions
expr2tc	pointer_expr (const BigInt &offset, const expr2t &object) const
expr2tc	object_rec (const BigInt &offset, const type2tc &pointer_type, const expr2tc &src) const

Protected Attributes
unsigned	null_object
unsigned	invalid_object

Member Typedef Documentation

obj_lookupt

typedef std::vector<expr2tc> pointer_logict::obj_lookupt

objectst

typedef std::unordered_map<expr2tc, unsigned int, irep2_hash> pointer_logict::objectst

Constructor & Destructor Documentation

~pointer_logict()

pointer_logict::~pointer_logict ( )

default

pointer_logict()

pointer_logict::pointer_logict

(

)

Member Function Documentation

add_object()

unsigned pointer_logict::add_object

(

const expr2tc &

expr

)

get_free_obj_num()

unsigned pointer_logict::get_free_obj_num ( )

inline

get_invalid_object()

unsigned pointer_logict::get_invalid_object ( ) const

inline

get_null_object()

unsigned pointer_logict::get_null_object ( ) const

inline

object_rec()

expr2tc pointer_logict::object_rec ( const BigInt & offset, const type2tc & pointer_type, const expr2tc & src ) const

protected

pointer_expr() [1/3]

expr2tc pointer_logict::pointer_expr ( const BigInt & offset, const expr2t & object ) const

protected

pointer_expr() [2/3]

expr2tc pointer_logict::pointer_expr	(	const pointert &	pointer,
		const type2tc &	type ) const

pointer_expr() [3/3]

expr2tc pointer_logict::pointer_expr	(	unsigned	object,
		const type2tc &	type ) const

Member Data Documentation

invalid_object

unsigned pointer_logict::invalid_object

protected

lookup

obj_lookupt pointer_logict::lookup

null_object

unsigned pointer_logict::null_object

protected

obj_num_offset

unsigned int pointer_logict::obj_num_offset

objects

objectst pointer_logict::objects

---

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

• src/solvers/prop/pointer_logic.h
• src/solvers/prop/pointer_logic.cpp