dereferencet Class Reference

Class containing expression dereference logic. More...

#include <dereference.h>

Classes
struct	modet
	The different ways in which a pointer may be accessed. More...
class	quantifier_scopet
	Records what a forall2t/exists2t binds while its body is walked, so the index fold in dereference_expr_nonscalar leaves the bound variable alone: the rename callback carries no quantifier context and would substitute the like-named program variable's SSA value (rename_quantified guards the same concern at the renaming layer, #7024). More...

Public Member Functions
	dereferencet (const namespacet &_ns, contextt &_new_context, const optionst &_options, dereference_callbackt &_dereference_callback)
	Primary constructor.
virtual	~dereferencet ()=default
virtual void	dereference_expr (expr2tc &expr, guard2tc &guard, modet mode)
	Take an expression and dereference it.
virtual expr2tc	dereference (const expr2tc &dest, const type2tc &type, const guard2tc &guard, modet mode, const expr2tc &extra_offset)
bool	has_dereference (const expr2tc &expr) const
	Does the given expression have a dereference in it somewhere?
void	build_reference_rec (expr2tc &value, const expr2tc &offset, const type2tc &type, const guard2tc &guard, modet mode, unsigned long alignment=0)
void	set_block_assertions (void)
void	clear_block_assertions (void)

Static Public Member Functions
static void	reset_object_counter ()
	Zero the failed-symbol counter.

Static Public Attributes
static const constexpr modet	READ = {modet::READ, false}
static const constexpr modet	WRITE = {modet::WRITE, false}
static const constexpr modet	FREE = {modet::FREE, false}
static const constexpr modet	INTERNAL = {modet::INTERNAL, false}

Detailed Description

Class containing expression dereference logic.

This class doesn't actually store any state, in that all the side-effects of what it does are either returned to the caller, or passed through the dereference_callbackt object's virtual methods. Members of this class only exist to provide context to the dereference being performed.

Constructor & Destructor Documentation

dereferencet()

dereferencet::dereferencet ( const namespacet & _ns, contextt & _new_context, const optionst & _options, dereference_callbackt & _dereference_callback )

inline

Primary constructor.

Parameters

_ns	Namespace to make type lookups against
_new_context	Context to store new (failed) symbols in.
_options	Options to behave under (i.e., disable ptr checks etc).
_dereference_callback	Callback object to invoke when we need external information or otherwise need to interacte with the context.

~dereferencet()

virtual dereferencet::~dereferencet ( )

virtualdefault

Member Function Documentation

build_reference_rec()

void dereferencet::build_reference_rec	(	expr2tc &	value,
		const expr2tc &	offset,
		const type2tc &	type,
		const guard2tc &	guard,
		modet	mode,
		unsigned long	alignment = 0 )

clear_block_assertions()

void dereferencet::clear_block_assertions ( void )

inline

dereference()

expr2tc dereferencet::dereference ( const expr2tc & dest, const type2tc & type, const guard2tc & guard, modet mode, const expr2tc & extra_offset )

virtual

dereference_expr()

void dereferencet::dereference_expr ( expr2tc & expr, guard2tc & guard, modet mode )

virtual

Take an expression and dereference it.

This will descend through the whole of the expression given, and dereference any dereferences contained within it. The given expr will be modified in place. It also doesn't necessarily have to contain a dereference at all (in which case nothing will happen), or start at a relevant part of the expression, as this method will recurse through the whole thing.

Parameters

expr	The expression to be dereferenced.
guard	Guard to be added to any dereference failure assertions generated.
The	way in which this dereference is being accessed. Only affects the assertions that are generated.

has_dereference()

bool dereferencet::has_dereference

(

const expr2tc &

expr

)

const

Does the given expression have a dereference in it somewhere?

Parameters

expr	The expression to check for existence of a dereference.

Returns

True when the given expression does have a dereference.

reset_object_counter()

void dereferencet::reset_object_counter ( )

static

Zero the failed-symbol counter.

Called once per exploration from reachability_treet::setup_for_new_explore, so the equation is a function of (program, options) alone (R15).

set_block_assertions()

void dereferencet::set_block_assertions ( void )

inline

Member Data Documentation

FREE

const constexpr modet dereferencet::FREE = {modet::FREE, false}

staticconstexpr

INTERNAL

const constexpr modet dereferencet::INTERNAL = {modet::INTERNAL, false}

staticconstexpr

READ

const constexpr modet dereferencet::READ = {modet::READ, false}

staticconstexpr

WRITE

const constexpr modet dereferencet::WRITE = {modet::WRITE, false}

staticconstexpr

---

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

• src/pointer-analysis/dereference.h
• src/pointer-analysis/dereference.cpp