cprover
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 
16 
17 #include "goto_symex.h"
18 
21 {
22 public:
24  goto_symext &_goto_symex,
25  goto_symext::statet &_state):
26  goto_symex(_goto_symex),
27  state(_state)
28  {
29  }
30 
31 protected:
34 
35  void
36  get_value_set(const exprt &expr, value_setst::valuest &value_set) override;
37 
38  bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override;
39 };
40 
41 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:33
symex_dereference_statet::has_failed_symbol
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
Definition: symex_dereference_state.cpp:16
goto_symex_statet
Definition: goto_symex_state.h:34
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:27
exprt
Base class for all expressions.
Definition: expr.h:54
symex_dereference_statet::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &value_set) override
Definition: symex_dereference_state.cpp:71
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
goto_symex.h
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:78
symex_dereference_statet
Definition: symex_dereference_state.h:19
symbolt
Symbol table entry.
Definition: symbol.h:27
dereference_callback.h
symex_dereference_statet::goto_symex
goto_symext & goto_symex
Definition: symex_dereference_state.h:32
symex_dereference_statet::symex_dereference_statet
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
Definition: symex_dereference_state.h:23