CBMC
Loading...
Searching...
No Matches
Public Member Functions | List of all members
dereference_callbackt Class Referenceabstract

Base class for pointer value set analysis. More...

#include <dereference_callback.h>

+ Inheritance diagram for dereference_callbackt:
[フレーム]
[legend]

Public Member Functions

virtual  ~dereference_callbackt ()=default
 
virtual std::vector< exprt >  get_value_set (const exprt &expr) const =0
 
virtual const symbolt *  get_or_create_failed_symbol (const exprt &expr)=0
 

Detailed Description

Base class for pointer value set analysis.

Implemented by goto_program_dereferencet. This exists so that value_set_dereferencet can contain a reference to goto_program_derefencet which cannot be done directly because goto_program_derefencet contains a value_set_dereferencet .

Definition at line 27 of file dereference_callback.h.

Constructor & Destructor Documentation

◆  ~dereference_callbackt()

virtual dereference_callbackt::~dereference_callbackt ( )
virtualdefault

Member Function Documentation

◆  get_or_create_failed_symbol()

virtual const symbolt * dereference_callbackt::get_or_create_failed_symbol ( const exprt &  expr )
pure virtual

Implemented in symex_dereference_statet, and goto_program_dereferencet.

◆  get_value_set()

virtual std::vector< exprt > dereference_callbackt::get_value_set ( const exprt &  expr ) const
pure virtual

Implemented in symex_dereference_statet, and goto_program_dereferencet.

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

AltStyle によって変換されたページ (->オリジナル) /