Loading...

Searching...

No Matches

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:

[フレーム]

[legend]

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.

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

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

~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:

/home/runner/work/cbmc/cbmc/src/solvers/flattening/pointer_logic.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/pointer_logic.cpp