CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_dereference_state.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
13#define CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
14
16
17#include "goto_symex.h"
18
26{
27public:
32
33protected:
35 const namespacet &ns;
36
37 std::vector<exprt> get_value_set(const exprt &expr) const override;
38
39 const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
40};
41
42#endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for pointer value set analysis.
Base class for all expressions.
Definition expr.h:56
Central data structure: state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Symbol table entry.
Definition symbol.h:28
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
std::vector< exprt > get_value_set(const exprt &expr) const override
Just forwards a value-set query to state.value_set
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Pointer Dereferencing.
Symbolic Execution.