Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value sets (from goto-symex's working value set) and retrieve or create failed symbols on demand. More...

#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::statet &_state, const namespacet &ns)

Public Member Functions inherited from dereference_callbackt
virtual	~dereference_callbackt ()=default

Protected Member Functions
std::vector< exprt >	get_value_set (const exprt &expr) const override
	Just forwards a value-set query to `state.value_set` More...

const symbolt *	get_or_create_failed_symbol (const exprt &expr) override
	Get or create a failed symbol for the given pointer-typed expression. More...

Protected Attributes
goto_symext::statet &	state

const namespacet &	ns

Detailed Description

Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value sets (from goto-symex's working value set) and retrieve or create failed symbols on demand.

For details of symex-dereference's operation see goto_symext::dereference

Definition at line 24 of file symex_dereference_state.h.

Constructor & Destructor Documentation

◆ symex_dereference_statet()

symex_dereference_statet::symex_dereference_statet	(	goto_symext::statet &	_state,
		const namespacet &	ns
	)

inline

Definition at line 28 of file symex_dereference_state.h.

Member Function Documentation

◆ get_or_create_failed_symbol()

const symbolt * symex_dereference_statet::get_or_create_failed_symbol ( const exprt & expr )

overrideprotectedvirtual

Get or create a failed symbol for the given pointer-typed expression.

These are used as placeholders when dereferencing expressions that are illegal to dereference, such as null pointers. The add_failed_symbols pass must have been run for this to do anything useful; it annotates a pointer-typed symbol p with an ID_C_failed_symbol comment, which we then clone on demand due to L1 renaming.

For example, if expr is p and it has an ID_C_failed_symbol p$object (the naming convention used by add_failed_symbols), and the latest L1 renaming of p is p!2@4, then we will create p$object!2@4 if it doesn't already exist.

Parameters

expr	expression to get or create a failed symbol for

Returns: pointer to the failed symbol for expr, or nullptr if none

Implements dereference_callbackt.

Definition at line 29 of file symex_dereference_state.cpp.

◆ get_value_set()

std::vector< exprt > symex_dereference_statet::get_value_set ( const exprt & expr ) const

overrideprotectedvirtual

Just forwards a value-set query to state.value_set

Implements dereference_callbackt.

Definition at line 79 of file symex_dereference_state.cpp.

Member Data Documentation

◆ ns

const namespacet& symex_dereference_statet::ns

protected

Definition at line 35 of file symex_dereference_state.h.

◆ state

goto_symext::statet& symex_dereference_statet::state

protected

Definition at line 34 of file symex_dereference_state.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/symex_dereference_state.h
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_dereference_state.cpp

Public Member Functions

Protected Member Functions

Protected Attributes