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  virtual void dereference_failure(
36  const std::string &property,
37  const std::string &msg,
38  const guardt &guard);
39 
40  virtual void get_value_set(
41  const exprt &expr,
42  value_setst::valuest &value_set);
43 
44  virtual bool has_failed_symbol(
45  const exprt &expr,
46  const symbolt *&symbol);
47 };
48 
49 #endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
Pointer Dereferencing.
Definition: guard.h:19
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symex_dereference_statet(goto_symext &_goto_symex, goto_symext::statet &_state)
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)
Symbolic Execution.
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
The main class for the forward symbolic simulator.
Definition: goto_symex.h:41
Base class for all expressions.
Definition: expr.h:46
std::list< exprt > valuest
Definition: value_sets.h:28