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
Base class for pointer value set analysis.
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
void get_value_set(const exprt &expr, value_setst::valuest &value_set) override
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
The main class for the forward symbolic simulator.
Base class for all expressions.
std::list< exprt > valuest