cprover
|
Base class for pointer value set analysis. More...
#include <dereference_callback.h>
Public Member Functions | |
virtual | ~dereference_callbackt ()=default |
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 |
Base class for pointer value set analysis.
Implemented by goto_program_dereferencet. This exists so that value_set_dereferencet
can contain a reference to goto_program_derefencet
which cannot be done directly because goto_program_derefencet
contains a value_set_dereferencet
.
Definition at line 27 of file dereference_callback.h.
|
virtualdefault |
|
pure virtual |
Implemented in goto_program_dereferencet, and symex_dereference_statet.
|
pure virtual |
Implemented in goto_program_dereferencet, and symex_dereference_statet.