symex_dereference_state.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution of ANSI-C
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
#define CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H
 
#include <pointer-analysis/dereference_callback.h>
 
#include "goto_symex.h"

class symex_dereference_statet:
  public dereference_callbackt
{
public:
  symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
    : state(_state), ns(ns)
  {
  }
 
protected:
  goto_symext::statet &state;
  const namespacet &ns;
 
  std::vector<exprt> get_value_set(const exprt &expr) const override;
 
  const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
};
 
#endif // CPROVER_GOTO_SYMEX_SYMEX_DEREFERENCE_STATE_H