CBMC
symex_dereference_state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: 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 
15 #include <pointer-analysis/dereference_callback.h>
16 
17 #include "goto_symex.h"
18 
24 class symex_dereference_statet:
25  public dereference_callbackt
26 {
27 public:
28  symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
29  : state(_state), ns(ns)
30  {
31  }
32 
33 protected:
34  goto_symext::statet &state;
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
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:28
exprt
Base class for all expressions.
Definition: expr.h:56
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:43
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
symbolt
Symbol table entry.
Definition: symbol.h:28
symex_dereference_statet
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Definition: symex_dereference_state.h:26
symex_dereference_statet::ns
const namespacet & ns
Definition: symex_dereference_state.h:35
symex_dereference_statet::symex_dereference_statet
symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
Definition: symex_dereference_state.h:28
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:34
symex_dereference_statet::get_value_set
std::vector< exprt > get_value_set(const exprt &expr) const override
Just forwards a value-set query to state.value_set
Definition: symex_dereference_state.cpp:79
symex_dereference_statet::get_or_create_failed_symbol
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Definition: symex_dereference_state.cpp:29
dereference_callback.h
Pointer Dereferencing.
goto_symex.h
Symbolic Execution.