goto_program_dereferencet Class Reference

#include <goto_program_dereference.h>

Inheritance diagram for goto_program_dereferencet:

Public Member Functions
	goto_program_dereferencet (const namespacet &_ns, contextt &_new_context, const optionst &_options, value_setst &_value_sets)
void	dereference_program (goto_programt &goto_program, bool checks_only=false)
void	dereference_program (goto_functionst &goto_functions, bool checks_only=false)
void	pointer_checks (goto_programt &goto_program)
void	pointer_checks (goto_functionst &goto_functions)
void	dereference_expression (goto_programt::const_targett target, expr2tc &expr)
	~goto_program_dereferencet () override=default

Protected Member Functions
bool	has_failed_symbol (const expr2tc &expr, const symbolt *&symbol) override
	Check whether a failed symbol already exists for the given symbol.
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
bool	is_live_variable (const expr2tc &sym) override
	Determine whether variable is "alive".
void	get_value_set (const expr2tc &expr, value_setst::valuest &dest) override
	Fetch the set of values that the given pointer variable can point at.
void	dereference_instruction (goto_programt::targett target, bool checks_only=false)
void	dereference_expr (expr2tc &expr, const bool checks_only, const dereferencet::modet mode)
Protected Member Functions inherited from dereference_callbackt
virtual	~dereference_callbackt ()=default
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)

Protected Attributes
const optionst &	options
const namespacet &	ns
value_setst &	value_sets
dereferencet	dereference
locationt	dereference_location
goto_programt::const_targett	current_target
std::set< expr2tc >	assertions
std::set< expr2tc >	assumptions
goto_programt	new_code

Constructor & Destructor Documentation

goto_program_dereferencet()

goto_program_dereferencet::goto_program_dereferencet ( const namespacet & _ns, contextt & _new_context, const optionst & _options, value_setst & _value_sets )

inline

~goto_program_dereferencet()

goto_program_dereferencet::~goto_program_dereferencet ( )

overridedefault

Member Function Documentation

dereference_assume()

void goto_program_dereferencet::dereference_assume ( const guard2tc & guard )

overrideprotectedvirtual

Implements dereference_callbackt.

dereference_expr()

void goto_program_dereferencet::dereference_expr ( expr2tc & expr, const bool checks_only, const dereferencet::modet mode )

protected

dereference_expression()

void goto_program_dereferencet::dereference_expression	(	goto_programt::const_targett	target,
		expr2tc &	expr )

dereference_failure()

void goto_program_dereferencet::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.

dereference_instruction()

void goto_program_dereferencet::dereference_instruction ( goto_programt::targett target, bool checks_only = false )

protected

dereference_program() [1/2]

void goto_program_dereferencet::dereference_program	(	goto_functionst &	goto_functions,
		bool	checks_only = false )

dereference_program() [2/2]

void goto_program_dereferencet::dereference_program	(	goto_programt &	goto_program,
		bool	checks_only = false )

get_value_set()

void goto_program_dereferencet::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 goto_program_dereferencet::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 goto_program_dereferencet::is_live_variable ( const expr2tc & sym )

inlineoverrideprotectedvirtual

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.

pointer_checks() [1/2]

void goto_program_dereferencet::pointer_checks

(

goto_functionst &

goto_functions

)

pointer_checks() [2/2]

void goto_program_dereferencet::pointer_checks

(

goto_programt &

goto_program

)

Member Data Documentation

assertions

std::set<expr2tc> goto_program_dereferencet::assertions

protected

assumptions

std::set<expr2tc> goto_program_dereferencet::assumptions

protected

current_target

goto_programt::const_targett goto_program_dereferencet::current_target

protected

dereference

dereferencet goto_program_dereferencet::dereference

protected

dereference_location

locationt goto_program_dereferencet::dereference_location

protected

new_code

goto_programt goto_program_dereferencet::new_code

protected

ns

const namespacet& goto_program_dereferencet::ns

protected

options

const optionst& goto_program_dereferencet::options

protected

value_sets

value_setst& goto_program_dereferencet::value_sets

protected

---

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

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