cprover
|
TO_BE_DOCUMENTED. More...
#include <dereference_callback.h>
Public Member Functions | |
virtual | ~dereference_callbackt () |
virtual void | dereference_failure (const std::string &property, const std::string &msg, const guardt &guard)=0 |
virtual void | get_value_set (const exprt &expr, value_setst::valuest &value_set)=0 |
virtual bool | has_failed_symbol (const exprt &expr, const symbolt *&symbol)=0 |
TO_BE_DOCUMENTED.
Definition at line 25 of file dereference_callback.h.
|
virtual |
Definition at line 14 of file dereference_callback.cpp.
|
pure virtual |
Implemented in goto_program_dereferencet, and symex_dereference_statet.
Referenced by value_set_dereferencet::bounds_check(), value_set_dereferencet::build_reference_to(), value_set_dereferencet::invalid_pointer(), value_set_dereferencet::memory_model_bytes(), value_set_dereferencet::memory_model_conversion(), and value_set_dereferencet::valid_check().
|
pure virtual |
Implemented in goto_program_dereferencet, and symex_dereference_statet.
Referenced by value_set_dereferencet::dereference().
|
pure virtual |
Implemented in goto_program_dereferencet, and symex_dereference_statet.
Referenced by value_set_dereferencet::dereference().