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
46 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
goto_symext::statet & state
Central data structure: state.
Base class for pointer value set analysis.
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
#define SINCE(year, month, day, msg)
void get_value_set(const exprt &expr, value_setst::valuest &value_set) const override
Just forwards a value-set query to state.value_set
symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)