cprover
|
#include <pointer_logic.h>
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. More... | |
exprt | pointer_expr (std::size_t object, const pointer_typet &type) const |
Convert an (object,0) pair to an expression. More... | |
~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 | |
hash_numbering< exprt, irep_hash > | objects |
Protected Attributes | |
const namespacet & | ns |
std::size_t | null_object |
std::size_t | invalid_object |
Definition at line 22 of file pointer_logic.h.
pointer_logict::~pointer_logict | ( | ) |
Definition at line 163 of file pointer_logic.cpp.
|
explicit |
Definition at line 153 of file pointer_logic.cpp.
std::size_t pointer_logict::add_object | ( | const exprt & | expr | ) |
Definition at line 43 of file pointer_logic.cpp.
void pointer_logict::get_dynamic_objects | ( | std::vector< std::size_t > & | objects | ) | const |
Definition at line 33 of file pointer_logic.cpp.
|
inline |
Definition at line 64 of file pointer_logic.h.
|
inline |
Definition at line 58 of file pointer_logic.h.
bool pointer_logict::is_dynamic_object | ( | const exprt & | expr | ) | const |
Definition at line 24 of file pointer_logic.cpp.
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.
exprt pointer_logict::pointer_expr | ( | std::size_t | object, |
const pointer_typet & | type | ||
) | const |
Convert an (object,0) pair to an expression.
Definition at line 59 of file pointer_logic.cpp.
|
protected |
Definition at line 75 of file pointer_logic.h.
|
protected |
Definition at line 74 of file pointer_logic.h.
|
protected |
Definition at line 75 of file pointer_logic.h.
hash_numbering<exprt, irep_hash> pointer_logict::objects |
Definition at line 26 of file pointer_logic.h.