cprover
|
#include <pointer_logic.h>
Classes | |
struct | pointert |
Public Types | |
typedef hash_numbering< exprt, irep_hash > | objectst |
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 |
Protected Attributes | |
const namespacet & | ns |
std::size_t | null_object |
std::size_t | invalid_object |
Definition at line 22 of file pointer_logic.h.
typedef hash_numbering<exprt, irep_hash> pointer_logict::objectst |
Definition at line 26 of file pointer_logic.h.
pointer_logict::~pointer_logict | ( | ) |
Definition at line 155 of file pointer_logic.cpp.
|
explicit |
Definition at line 145 of file pointer_logic.cpp.
std::size_t pointer_logict::add_object | ( | const exprt & | expr | ) |
Definition at line 49 of file pointer_logic.cpp.
void pointer_logict::get_dynamic_objects | ( | std::vector< std::size_t > & | objects | ) | const |
Definition at line 36 of file pointer_logic.cpp.
|
inline |
Definition at line 65 of file pointer_logic.h.
|
inline |
Definition at line 59 of file pointer_logic.h.
bool pointer_logict::is_dynamic_object | ( | const exprt & | expr | ) | const |
Definition at line 23 of file pointer_logic.cpp.
exprt pointer_logict::pointer_expr | ( | const pointert & | pointer, |
const pointer_typet & | type | ||
) | const |
Definition at line 73 of file pointer_logic.cpp.
exprt pointer_logict::pointer_expr | ( | std::size_t | object, |
const pointer_typet & | type | ||
) | const |
Definition at line 65 of file pointer_logic.cpp.
|
protected |
|
protected |
Definition at line 76 of file pointer_logic.h.
|
protected |
Definition at line 75 of file pointer_logic.h.
|
protected |
Definition at line 76 of file pointer_logic.h.
objectst pointer_logict::objects |
Definition at line 27 of file pointer_logic.h.