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
Base class for pointer value set analysis.
Pointer Dereferencing.
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
Symbol table entry.
Definition: symbol.h:27
void get_value_set(const exprt &expr, value_setst::valuest &value_set) override
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
Symbolic Execution.
The main class for the forward symbolic simulator.
Definition: goto_symex.h:78
Base class for all expressions.
Definition: expr.h:54
std::list< exprt > valuest
Definition: value_sets.h:28