Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
41 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
goto_symext::statet & state
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
Base class for pointer value set analysis.
Base class for all expressions.
void get_value_set(const exprt &expr, value_setst::valuest &value_set) override
std::list< exprt > valuest
The main class for the forward symbolic simulator.
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)