symex_dereference_statet Class Reference

#include <goto_symex.h>

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

Protected Attributes
goto_symext &	goto_symex
goto_symext::statet &	state

Constructor & Destructor Documentation

symex_dereference_statet()

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

inline

Member Function Documentation

dereference_assume()

void symex_dereference_statet::dereference_assume ( const guard2tc & guard )

overrideprotectedvirtual

Implements dereference_callbackt.

dereference_failure()

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

overrideprotectedvirtual

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.

Implements dereference_callbackt.

dump_internal_state()

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

overrideprotectedvirtual

Reimplemented from dereference_callbackt.

get_value_set()

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

overrideprotectedvirtual

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.

Implements dereference_callbackt.

has_failed_symbol()

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

overrideprotectedvirtual

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

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

Implements dereference_callbackt.

is_live_variable()

bool symex_dereference_statet::is_live_variable ( const expr2tc & sym )

overrideprotectedvirtual

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

Implements dereference_callbackt.

rename()

void symex_dereference_statet::rename ( expr2tc & expr )

overrideprotectedvirtual

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 from dereference_callbackt.

Member Data Documentation

goto_symex

goto_symext& symex_dereference_statet::goto_symex

protected

state

goto_symext::statet& symex_dereference_statet::state

protected

---

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

• src/goto-symex/engine/goto_symex.h
• src/goto-symex/engine/symex_dereference.cpp