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_table_baset &_new_symbol_table, const optionst &_options, value_setst &_value_sets, message_handlert &message_handler)

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

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

void	dereference_expression (const irep_idt &function_id, 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
const symbolt *	get_or_create_failed_symbol (const exprt &expr) override

std::vector< exprt >	get_value_set (const exprt &expr) const 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)
	Turn subexpression of `expr` of the form `&p` into p and use `dereference` on subexpressions of the form `p` More...

void	dereference_expr (exprt &expr, const bool checks_only)
	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

irep_idt	current_function

goto_programt::const_targett	current_target

goto_programt	new_code

Detailed Description

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

Definition at line 29 of file goto_program_dereference.h.

Constructor & Destructor Documentation

◆ goto_program_dereferencet()

goto_program_dereferencet::goto_program_dereferencet	(	const namespacet &	_ns,
		symbol_table_baset &	_new_symbol_table,
		const optionst &	_options,
		value_setst &	_value_sets,
		message_handlert &	message_handler
	)

inline

Definition at line 43 of file goto_program_dereference.h.

◆ ~goto_program_dereferencet()

virtual goto_program_dereferencet::~goto_program_dereferencet ( )

inlinevirtual

Definition at line 69 of file goto_program_dereference.h.

Member Function Documentation

◆ dereference_expr()

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

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.

Definition at line 145 of file goto_program_dereference.cpp.

◆ dereference_expression()

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

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

Definition at line 247 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 195 of file goto_program_dereference.cpp.

◆ dereference_program() [1/2]

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

Definition at line 180 of file goto_program_dereference.cpp.

◆ dereference_program() [2/2]

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

Definition at line 158 of file goto_program_dereference.cpp.

◆ dereference_rec()

void goto_program_dereferencet::dereference_rec ( exprt & expr )

protected

Turn subexpression of expr of the form &*p into p and use dereference on subexpressions of the form *p

Parameters

expr	expression in which to remove dereferences

Definition at line 50 of file goto_program_dereference.cpp.

◆ get_or_create_failed_symbol()

const symbolt * goto_program_dereferencet::get_or_create_failed_symbol ( const exprt & expr )

overrideprotectedvirtual

Parameters

expr	expression to check

Returns: pointer to appropriate failed symbol for expr, or nullptr if none

Implements dereference_callbackt.

Definition at line 25 of file goto_program_dereference.cpp.

◆ get_value_set()

std::vector< exprt > goto_program_dereferencet::get_value_set ( const exprt & expr ) const

overrideprotectedvirtual

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

Parameters

expr	an expression

Returns: the value set

Implements dereference_callbackt.

Definition at line 135 of file goto_program_dereference.cpp.

Member Data Documentation

◆ current_function

irep_idt goto_program_dereferencet::current_function

protected

Definition at line 91 of file goto_program_dereference.h.

◆ current_target

goto_programt::const_targett goto_program_dereferencet::current_target

protected

Definition at line 92 of file goto_program_dereference.h.

◆ dereference

value_set_dereferencet goto_program_dereferencet::dereference

protected

Definition at line 77 of file goto_program_dereference.h.

◆ new_code

goto_programt goto_program_dereferencet::new_code

protected

Definition at line 93 of file goto_program_dereference.h.

◆ ns

const namespacet& goto_program_dereferencet::ns

protected

Definition at line 75 of file goto_program_dereference.h.

◆ options

const optionst& goto_program_dereferencet::options

protected

Definition at line 74 of file goto_program_dereference.h.

◆ value_sets

value_setst& goto_program_dereferencet::value_sets

protected

Definition at line 76 of file goto_program_dereference.h.

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

/home/runner/work/cbmc/cbmc/src/pointer-analysis/goto_program_dereference.h
/home/runner/work/cbmc/cbmc/src/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_instruction()

◆ dereference_program() [1/2]

◆ dereference_program() [2/2]

◆ dereference_rec()

◆ get_or_create_failed_symbol()

◆ get_value_set()

Member Data Documentation

◆ current_function

◆ current_target

◆ dereference

◆ new_code

◆ ns

◆ options

◆ value_sets