dereference_callbackt Class Reference

Class providing interface to value set tracking code. More...

#include <dereference.h>

Inheritance diagram for dereference_callbackt:

Classes
struct	internal_item

Public Member Functions
virtual	~dereference_callbackt ()=default
virtual void	dereference_failure (const std::string &property, const std::string &msg, const guard2tc &guard)=0
	Encode a dereference failure assertion.
virtual void	dereference_assume (const guard2tc &guard)=0
virtual void	get_value_set (const expr2tc &expr, value_setst::valuest &value_set)=0
	Fetch the set of values that the given pointer variable can point at.
virtual bool	has_failed_symbol (const expr2tc &expr, const symbolt *&symbol)=0
	Check whether a failed symbol already exists for the given symbol.
virtual void	rename (expr2tc &expr)
	Rename the given expression into the callback's current execution context.
virtual void	dump_internal_state (const std::list< struct internal_item > &data)
virtual bool	is_live_variable (const expr2tc &sym)=0
	Determine whether variable is "alive".

Detailed Description

Class providing interface to value set tracking code.

This class allows dereference code to get more data out of the environment in which it is dereferencing, fetching the set of values that a pointer points at, and also encoding any assertions that occur regarding the validity of the dereference.

Constructor & Destructor Documentation

~dereference_callbackt()

virtual dereference_callbackt::~dereference_callbackt ( )

virtualdefault

Member Function Documentation

dereference_assume()

virtual void dereference_callbackt::dereference_assume ( const guard2tc & guard )

pure virtual

Implemented in goto_program_dereferencet, and symex_dereference_statet.

dereference_failure()

virtual void dereference_callbackt::dereference_failure ( const std::string & property, const std::string & msg, const guard2tc & guard )

pure virtual

Encode a dereference failure assertion.

If a dereference does, or can trigger undefined or illegal behavior, then this method is called to record it so that it can be asserted against.

Parameters

property	Classification of the assertion being violated.
msg	Description of the reason for this assertion.
guard	Guard for this assertion – evaluates to true whe this assertion has been violated.

Implemented in goto_program_dereferencet, and symex_dereference_statet.

dump_internal_state()

virtual void dereference_callbackt::dump_internal_state ( const std::list< struct internal_item > & data )

inlinevirtual

Reimplemented in symex_dereference_statet.

get_value_set()

virtual void dereference_callbackt::get_value_set ( const expr2tc & expr, value_setst::valuest & value_set )

pure virtual

Fetch the set of values that the given pointer variable can point at.

Parameters

expr	Pointer symbol to get the value set of.
value_set	A value set to store the output of this call into.

Implemented in goto_program_dereferencet, and symex_dereference_statet.

has_failed_symbol()

virtual bool dereference_callbackt::has_failed_symbol ( const expr2tc & expr, const symbolt *& symbol )

pure virtual

Check whether a failed symbol already exists for the given symbol.

This is legacy, and will be removed at some point soon.

Implemented in goto_program_dereferencet, and symex_dereference_statet.

is_live_variable()

virtual bool dereference_callbackt::is_live_variable ( const expr2tc & sym )

pure virtual

Determine whether variable is "alive".

For function-local variable symbols, determine whether or not a pointer to the corresponding l1 storage is considered live: if the corresponding activation record has been left, then it isn't.

Parameters

sym	Symbol to check validity of.

Returns

True if variable is alive

Implemented in goto_program_dereferencet, and symex_dereference_statet.

rename()

virtual void dereference_callbackt::rename ( expr2tc & expr )

inlinevirtual

Rename the given expression into the callback's current execution context.

The default implementation is a no-op; the symbolic-execution override substitutes the SSA names and recorded constants symex currently holds. Called on the index operands of dereference chains once their inner dereferences are resolved, so an index whose value symex knows folds to a constant and the access stays on the constant-offset path (see dereference_expr_nonscalar, #7311). Indices mentioning a symbol bound by an enclosing quantifier are excluded, as is the whole body of a quantifier whose binder names no symbol: the callback has no quantifier context and would substitute the like-named program variable's value.

Parameters

expr	An expression to be renamed

Reimplemented in symex_dereference_statet.

---

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

• src/pointer-analysis/dereference.h