cprover
|
#include <symex_dereference_state.h>
Public Member Functions | |
symex_dereference_statet (goto_symext &_goto_symex, goto_symext::statet &_state) | |
![]() | |
virtual | ~dereference_callbackt () |
Protected Member Functions | |
virtual void | dereference_failure (const std::string &property, const std::string &msg, const guardt &guard) |
virtual void | get_value_set (const exprt &expr, value_setst::valuest &value_set) |
virtual bool | has_failed_symbol (const exprt &expr, const symbolt *&symbol) |
Protected Attributes | |
goto_symext & | goto_symex |
goto_symext::statet & | state |
Definition at line 19 of file symex_dereference_state.h.
|
inline |
Definition at line 23 of file symex_dereference_state.h.
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 16 of file symex_dereference_state.cpp.
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 80 of file symex_dereference_state.cpp.
References from_expr(), value_sett::get_value_set(), goto_symex, goto_symext::ns, value_sett::output(), state, and goto_symex_statet::value_set.
|
protectedvirtual |
Implements dereference_callbackt.
Definition at line 23 of file symex_dereference_state.cpp.
References irept::get(), irept::get_bool(), symbol_exprt::get_identifier(), ssa_exprt::get_original_expr(), goto_symex, irept::id(), goto_symex_statet::L1, namespacet::lookup(), symbol_tablet::move(), symbolt::name, goto_symext::ns, goto_symex_statet::rename(), state, symbolt::symbol_expr(), goto_symex_statet::symbol_table, to_ssa_expr(), to_symbol_expr(), and symbolt::type.
|
protected |
Definition at line 32 of file symex_dereference_state.h.
Referenced by get_value_set(), and has_failed_symbol().
|
protected |
Definition at line 33 of file symex_dereference_state.h.
Referenced by get_value_set(), has_failed_symbol(), and goto_symext::symex_transition().