cprover
symex_dereference_statet Class Reference

#include <symex_dereference_state.h>

Inheritance diagram for symex_dereference_statet:
[legend]
Collaboration diagram for symex_dereference_statet:
[legend]

Public Member Functions

 symex_dereference_statet (goto_symext &_goto_symex, goto_symext::statet &_state)
 
- Public Member Functions inherited from dereference_callbackt
virtual ~dereference_callbackt ()
 

Protected Member Functions

virtual void dereference_failure (const std::string &property, const std::string &msg, const guardt &guard)
 
virtual void get_value_set (const exprt &expr, value_setst::valuest &value_set)
 
virtual bool has_failed_symbol (const exprt &expr, const symbolt *&symbol)
 

Protected Attributes

goto_symextgoto_symex
 
goto_symext::statetstate
 

Detailed Description

Definition at line 19 of file symex_dereference_state.h.

Constructor & Destructor Documentation

◆ symex_dereference_statet()

symex_dereference_statet::symex_dereference_statet ( goto_symext _goto_symex,
goto_symext::statet _state 
)
inline

Definition at line 23 of file symex_dereference_state.h.

Member Function Documentation

◆ dereference_failure()

void symex_dereference_statet::dereference_failure ( const std::string &  property,
const std::string &  msg,
const guardt guard 
)
protectedvirtual

Implements dereference_callbackt.

Definition at line 16 of file symex_dereference_state.cpp.

◆ get_value_set()

void symex_dereference_statet::get_value_set ( const exprt expr,
value_setst::valuest value_set 
)
protectedvirtual

◆ has_failed_symbol()

Member Data Documentation

◆ goto_symex

goto_symext& symex_dereference_statet::goto_symex
protected

Definition at line 32 of file symex_dereference_state.h.

Referenced by get_value_set(), and has_failed_symbol().

◆ state

goto_symext::statet& symex_dereference_statet::state
protected

The documentation for this class was generated from the following files: