12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H 36 const std::string &property,
37 const std::string &msg,
49 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H goto_symext::statet & state
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
The main class for the forward symbolic simulator.
Base class for all expressions.
std::list< exprt > valuest