cprover
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
symex_dereference_statet Class Reference

#include <symex_dereference_state.h>

+ Inheritance diagram for symex_dereference_statet:
+ Collaboration diagram for symex_dereference_statet:

Public Member Functions

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

Protected Member Functions

void get_value_set (const exprt &expr, value_setst::valuest &value_set) override
 
bool has_failed_symbol (const exprt &expr, const symbolt *&symbol) override
 

Protected Attributes

goto_symext & goto_symex
 
goto_symext::statet & state
 

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

◆ get_value_set()

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

Implements dereference_callbackt.

Definition at line 71 of file symex_dereference_state.cpp.

◆ has_failed_symbol()

bool symex_dereference_statet::has_failed_symbol ( const exprt &  expr,
const symbolt *&  symbol 
)
overrideprotectedvirtual

Implements dereference_callbackt.

Definition at line 16 of file symex_dereference_state.cpp.

Member Data Documentation

◆ goto_symex

goto_symext& symex_dereference_statet::goto_symex
protected

Definition at line 32 of file symex_dereference_state.h.

◆ state

goto_symext::statet& symex_dereference_statet::state
protected

Definition at line 33 of file symex_dereference_state.h.

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