Wrapper for functions removing dereferences in expressions contained in a goto program. More...

#include <goto_program_dereference.h>

Inheritance diagram for goto_program_dereferencet:

Collaboration diagram for goto_program_dereferencet:

Public Member Functions
	goto_program_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, 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)
	Throw an exception in case removing dereferences from the program would throw an exception. More...

void	pointer_checks (goto_functionst &goto_functions)
	Throw an exception in case removing dereferences from the program would throw an exception. More...

void	dereference_expression (goto_programt::const_targett target, exprt &expr)
	Set the current target to `target` and remove derefence from expr. More...

virtual	~goto_program_dereferencet ()

Protected Member Functions
virtual bool	is_valid_object (const irep_idt &identifier)

bool	has_failed_symbol (const exprt &expr, const symbolt *&symbol) override

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

void	get_value_set (const exprt &expr, value_setst::valuest &dest) override
	Gets the value set corresponding to the current target and expression `expr`. More...

void	dereference_instruction (goto_programt::targett target, bool checks_only=false)
	Remove dereference from expressions contained in the instruction at `target`. More...

void	dereference_rec (exprt &expr, guardt &guard, const value_set_dereferencet::modet mode)
	Turn subexpression of `expr` of the form `&p` or `reference_to(p)` to p and use `dereference` on subexpressions of the form `*p` More...

void	dereference_expr (exprt &expr, const bool checks_only, const value_set_dereferencet::modet mode)
	Remove dereference expressions contained in `expr`. More...

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

Protected Attributes
const optionst &	options

const namespacet &	ns

value_setst &	value_sets

value_set_dereferencet	dereference

goto_programt::const_targett	current_target

source_locationt	dereference_location
	Unused. More...

std::set< exprt >	assertions
	Unused. More...

goto_programt	new_code
	Unused. More...

Detailed Description

Wrapper for functions removing dereferences in expressions contained in a goto program.

Definition at line 24 of file goto_program_dereference.h.

Constructor & Destructor Documentation

◆ goto_program_dereferencet()

goto_program_dereferencet::goto_program_dereferencet	(	const namespacet &	_ns,
		symbol_tablet &	_new_symbol_table,
		const optionst &	_options,
		value_setst &	_value_sets
	)

inline

Definition at line 31 of file goto_program_dereference.h.

◆ ~goto_program_dereferencet()

virtual goto_program_dereferencet::~goto_program_dereferencet ( )

inlinevirtual

Definition at line 58 of file goto_program_dereference.h.

Member Function Documentation

◆ dereference_expr()

void goto_program_dereferencet::dereference_expr	(	exprt &	expr,
		const bool	checks_only,
		const value_set_dereferencet::modet	mode
	)

protected

Remove dereference expressions contained in expr.

Parameters

expr	an expression
checks_only	when true, execute the substitution on a copy of expr so that `expr` stays unchanged. In that case the only observable effect is whether an exception would be thrown.
mode	unused

Definition at line 250 of file goto_program_dereference.cpp.

◆ dereference_expression()

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

Set the current target to target and remove derefence from expr.

Definition at line 371 of file goto_program_dereference.cpp.

◆ dereference_failure()

void goto_program_dereferencet::dereference_failure	(	const std::string &	property,
		const std::string &	msg,
		const guardt &	guard
	)

protectedvirtual

Deprecated:

Definition at line 70 of file goto_program_dereference.cpp.

◆ dereference_instruction()

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

protected

Remove dereference from expressions contained in the instruction at target.

If check_only is true, the dereferencing is performed on copies of the expressions, in that case the only observable effect is whether an exception would be thrown.

Definition at line 305 of file goto_program_dereference.cpp.

◆ dereference_program() [1/2]

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

Definition at line 266 of file goto_program_dereference.cpp.

◆ dereference_program() [2/2]

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

Definition at line 290 of file goto_program_dereference.cpp.

◆ dereference_rec()

void goto_program_dereferencet::dereference_rec	(	exprt &	expr,
		guardt &	guard,
		const value_set_dereferencet::modet	mode
	)

protected

Turn subexpression of expr of the form &*p or reference_to(*p) to p and use dereference on subexpressions of the form *p

Parameters

expr	expression in which to remove dereferences
guard	boolean expression assumed to hold when dereferencing
mode	unused

Definition at line 104 of file goto_program_dereference.cpp.

◆ get_value_set()

void goto_program_dereferencet::get_value_set	(	const exprt &	expr,
		value_setst::valuest &	dest
	)

overrideprotectedvirtual

Gets the value set corresponding to the current target and expression expr.

Parameters

	expr	an expression
[out]	dest	gets the value set

Implements dereference_callbackt.

Definition at line 237 of file goto_program_dereference.cpp.

◆ has_failed_symbol()

bool goto_program_dereferencet::has_failed_symbol	(	const exprt &	expr,
		const symbolt *&	symbol
	)

overrideprotectedvirtual

Parameters

	expr	expression to check
[out]	symbol	symbol which gets assigned the value from the `failed_symbol` comment

Returns: true when expr is a symbol, whose type contains a failed_symbol comment which exists in the namespace.

Implements dereference_callbackt.

Definition at line 27 of file goto_program_dereference.cpp.

◆ is_valid_object()

bool goto_program_dereferencet::is_valid_object ( const irep_idt & identifier )

protectedvirtual

Deprecated:

Definition at line 50 of file goto_program_dereference.cpp.

◆ pointer_checks() [1/2]

void goto_program_dereferencet::pointer_checks ( goto_programt & goto_program )

Throw an exception in case removing dereferences from the program would throw an exception.

Definition at line 385 of file goto_program_dereference.cpp.

◆ pointer_checks() [2/2]

void goto_program_dereferencet::pointer_checks ( goto_functionst & goto_functions )

Throw an exception in case removing dereferences from the program would throw an exception.

Definition at line 393 of file goto_program_dereference.cpp.

Member Data Documentation

◆ assertions

std::set<exprt> goto_program_dereferencet::assertions

protected

Unused.

Definition at line 102 of file goto_program_dereference.h.

◆ current_target

goto_programt::const_targett goto_program_dereferencet::current_target

protected

Definition at line 96 of file goto_program_dereference.h.

◆ dereference

value_set_dereferencet goto_program_dereferencet::dereference

protected

Definition at line 66 of file goto_program_dereference.h.

◆ dereference_location

source_locationt goto_program_dereferencet::dereference_location

protected

Unused.

Definition at line 99 of file goto_program_dereference.h.

◆ new_code

goto_programt goto_program_dereferencet::new_code

protected

Unused.

Definition at line 105 of file goto_program_dereference.h.

◆ ns

const namespacet& goto_program_dereferencet::ns

protected

Definition at line 64 of file goto_program_dereference.h.

◆ options

const optionst& goto_program_dereferencet::options

protected

Definition at line 63 of file goto_program_dereference.h.

◆ value_sets

value_setst& goto_program_dereferencet::value_sets

protected

Definition at line 65 of file goto_program_dereference.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ goto_program_dereferencet()

◆ ~goto_program_dereferencet()

Member Function Documentation

◆ dereference_expr()

◆ dereference_expression()

◆ dereference_failure()

◆ dereference_instruction()

◆ dereference_program() [1/2]

◆ dereference_program() [2/2]

◆ dereference_rec()

◆ get_value_set()

◆ has_failed_symbol()

◆ is_valid_object()

◆ pointer_checks() [1/2]

◆ pointer_checks() [2/2]

Member Data Documentation

◆ assertions

◆ current_target

◆ dereference

◆ dereference_location

◆ new_code

◆ ns

◆ options

◆ value_sets