#include <goto_inline_class.h>

Collaboration diagram for goto_inlinet:

Classes
class	goto_inline_logt

Public Types
typedef goto_functionst::goto_functiont	goto_functiont
typedef std::pair< goto_programt::targett, bool >	callt
typedef std::list< callt >	call_listt
typedef std::map< irep_idt, call_listt >	inline_mapt

Public Member Functions
	goto_inlinet (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
	Sets up the class with the program to operate on.
void	goto_inline (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
	Inline all of the chosen calls in a given function.
void	goto_inline (const goto_inlinet::call_listt &call_list, goto_programt &goto_program, const bool force_full=false)
	Inline specified calls in a given program.
void	goto_inline (const inline_mapt &inline_map, const bool force_full=false)
	Inline all of the given call locations.
void	output_inline_map (std::ostream &out, const inline_mapt &inline_map)
void	output_cache (std::ostream &out) const
jsont	output_inline_log_json ()

Static Public Member Functions
static void	get_call (goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)

Protected Types
typedef goto_functionst::function_mapt	cachet
typedef std::unordered_set< irep_idt >	finished_sett
typedef std::unordered_set< irep_idt >	recursion_sett
typedef std::unordered_set< irep_idt >	no_body_sett

Protected Member Functions
void	goto_inline_nontransitive (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
const goto_functiont &	goto_inline_transitive (const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
bool	check_inline_map (const inline_mapt &inline_map) const
bool	check_inline_map (const irep_idt identifier, const inline_mapt &inline_map) const
bool	is_ignored (const irep_idt id) const
void	clear ()
void	expand_function_call (goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
	Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.
void	insert_function_body (const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
void	replace_return (goto_programt &body, const exprt &lhs)
void	parameter_assignments (const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst &parameter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
void	parameter_destruction (const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)

Protected Attributes
messaget	log
goto_functionst &	goto_functions
const namespacet &	ns
const bool	adjust_function
const bool	caching
goto_inline_logt	inline_log
cachet	cache
finished_sett	finished_set
recursion_sett	recursion_set
no_body_sett	no_body_set

Detailed Description

Definition at line 25 of file goto_inline_class.h.

Member Typedef Documentation

◆ cachet

typedef goto_functionst::function_mapt goto_inlinet::cachet

protected

Definition at line 216 of file goto_inline_class.h.

◆ call_listt

typedef std::list<callt> goto_inlinet::call_listt

Definition at line 57 of file goto_inline_class.h.

◆ callt

typedef std::pair<goto_programt::targett, bool> goto_inlinet::callt

Definition at line 54 of file goto_inline_class.h.

◆ finished_sett

typedef std::unordered_set<irep_idt> goto_inlinet::finished_sett

protected

Definition at line 219 of file goto_inline_class.h.

◆ goto_functiont

typedef goto_functionst::goto_functiont goto_inlinet::goto_functiont

Definition at line 49 of file goto_inline_class.h.

◆ inline_mapt

typedef std::map<irep_idt, call_listt> goto_inlinet::inline_mapt

Definition at line 60 of file goto_inline_class.h.

◆ no_body_sett

typedef std::unordered_set<irep_idt> goto_inlinet::no_body_sett

protected

Definition at line 225 of file goto_inline_class.h.

◆ recursion_sett

typedef std::unordered_set<irep_idt> goto_inlinet::recursion_sett

protected

Definition at line 222 of file goto_inline_class.h.

Constructor & Destructor Documentation

◆ goto_inlinet()

goto_inlinet::goto_inlinet	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		message_handlert &	message_handler,
		bool	adjust_function,
		bool	caching = true )

inline

Sets up the class with the program to operate on.

Parameters

goto_functions	: The map of functions to work on
ns	: The corresponding namespace
message_handler	: Used to log what is being inlined
adjust_function	Replace location in caller location.
caching	: cache functions when in transitive mode

Definition at line 35 of file goto_inline_class.h.

Member Function Documentation

◆ check_inline_map() [1/2]

bool goto_inlinet::check_inline_map ( const inline_mapt & inline_map ) const

protected

Definition at line 675 of file goto_inline_class.cpp.

◆ check_inline_map() [2/2]

bool goto_inlinet::check_inline_map	(	const irep_idt	identifier,
		const inline_mapt &	inline_map ) const

protected

Definition at line 627 of file goto_inline_class.cpp.

◆ clear()

void goto_inlinet::clear ( )

inlineprotected

Definition at line 176 of file goto_inline_class.h.

◆ expand_function_call()

void goto_inlinet::expand_function_call	(	goto_programt &	dest,
		const inline_mapt &	inline_map,
		const bool	transitive,
		const bool	force_full,
		goto_programt::targett	target )

protected

Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.

Definition at line 302 of file goto_inline_class.cpp.

◆ get_call()

void goto_inlinet::get_call	(	goto_programt::const_targett	target,
		exprt &	lhs,
		exprt &	function,
		exprt::operandst &	arguments )

static

Definition at line 432 of file goto_inline_class.cpp.

◆ goto_inline() [1/3]

void goto_inlinet::goto_inline	(	const goto_inlinet::call_listt &	call_list,
		goto_programt &	goto_program,
		const bool	force_full = false )

Inline specified calls in a given program.

Parameters

call_list	: calls to inline in the goto_program.
goto_program	: goto program to inline calls_list in.
force_full	: true to break recursion with a SKIP, false means detecting recursion is an error.

Definition at line 491 of file goto_inline_class.cpp.

◆ goto_inline() [2/3]

void goto_inlinet::goto_inline	(	const inline_mapt &	inline_map,
		const bool	force_full = false )

Inline all of the given call locations.

This is the highest-level interface and calls the other goto_inline

Parameters

inline_map	: which call locations to inline.
force_full	: true to break recursion with a SKIP, false means detecting recursion is an error.

Definition at line 450 of file goto_inline_class.cpp.

◆ goto_inline() [3/3]

void goto_inlinet::goto_inline	(	const irep_idt	identifier,
		goto_functiont &	goto_function,
		const inline_mapt &	inline_map,
		const bool	force_full = false )

Inline all of the chosen calls in a given function.

This is main entry point for the functionality

Parameters

identifier	: the name of the caller function.
goto_function	: the caller function itself.
inline_map	: which call locations to inline.
force_full	: true to break recursion with a SKIP, false means detecting recursion is an error.

Definition at line 476 of file goto_inline_class.cpp.

◆ goto_inline_nontransitive()

void goto_inlinet::goto_inline_nontransitive	(	const irep_idt	identifier,
		goto_functiont &	goto_function,
		const inline_mapt &	inline_map,
		const bool	force_full )

protected

Definition at line 506 of file goto_inline_class.cpp.

◆ goto_inline_transitive()

const goto_inlinet::goto_functiont & goto_inlinet::goto_inline_transitive	(	const irep_idt	identifier,
		const goto_functiont &	goto_function,
		const bool	force_full )

protected

Definition at line 558 of file goto_inline_class.cpp.

◆ insert_function_body()

void goto_inlinet::insert_function_body	(	const goto_functiont &	f,
		goto_programt &	dest,
		goto_programt::targett	target,
		const exprt &	lhs,
		const symbol_exprt &	function,
		const exprt::operandst &	arguments )

protected

Definition at line 214 of file goto_inline_class.cpp.

◆ is_ignored()

bool goto_inlinet::is_ignored ( const irep_idt id ) const

protected

Definition at line 620 of file goto_inline_class.cpp.

◆ output_cache()

void goto_inlinet::output_cache ( std::ostream & out ) const

Definition at line 727 of file goto_inline_class.cpp.

◆ output_inline_log_json()

jsont goto_inlinet::output_inline_log_json ( )

inline

Definition at line 94 of file goto_inline_class.h.

◆ output_inline_map()

void goto_inlinet::output_inline_map	(	std::ostream &	out,
		const inline_mapt &	inline_map )

Definition at line 686 of file goto_inline_class.cpp.

◆ parameter_assignments()

void goto_inlinet::parameter_assignments	(	const goto_programt::targett	target,
		const irep_idt &	function_name,
		const goto_functiont::parameter_identifierst &	parameter_identifiers,
		const exprt::operandst &	arguments,
		goto_programt &	dest )

protected

Definition at line 24 of file goto_inline_class.cpp.

◆ parameter_destruction()

void goto_inlinet::parameter_destruction	(	const goto_programt::targett	target,
		const goto_functiont::parameter_identifierst &	parameter_identifiers,
		goto_programt &	dest )

protected

Definition at line 125 of file goto_inline_class.cpp.

◆ replace_return()

void goto_inlinet::replace_return	(	goto_programt &	body,
		const exprt &	lhs )

protected

Definition at line 151 of file goto_inline_class.cpp.

Member Data Documentation

◆ adjust_function

const bool goto_inlinet::adjust_function

protected

Definition at line 153 of file goto_inline_class.h.

◆ cache

cachet goto_inlinet::cache

protected

Definition at line 217 of file goto_inline_class.h.

◆ caching

const bool goto_inlinet::caching

protected

Definition at line 154 of file goto_inline_class.h.

◆ finished_set

finished_sett goto_inlinet::finished_set

protected

Definition at line 220 of file goto_inline_class.h.

◆ goto_functions

goto_functionst& goto_inlinet::goto_functions

protected

Definition at line 150 of file goto_inline_class.h.

◆ inline_log

goto_inline_logt goto_inlinet::inline_log

protected

Definition at line 156 of file goto_inline_class.h.

◆ log

messaget goto_inlinet::log

protected

Definition at line 149 of file goto_inline_class.h.

◆ no_body_set

no_body_sett goto_inlinet::no_body_set

protected

Definition at line 226 of file goto_inline_class.h.

◆ ns

const namespacet& goto_inlinet::ns

protected

Definition at line 151 of file goto_inline_class.h.

◆ recursion_set

recursion_sett goto_inlinet::recursion_set

protected

Definition at line 223 of file goto_inline_class.h.

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

goto-programs/goto_inline_class.h
goto-programs/goto_inline_class.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ cachet

◆ call_listt

◆ callt

◆ finished_sett

◆ goto_functiont

◆ inline_mapt

◆ no_body_sett

◆ recursion_sett

Constructor & Destructor Documentation

◆ goto_inlinet()

Member Function Documentation

◆ check_inline_map() [1/2]

◆ check_inline_map() [2/2]

◆ clear()

◆ expand_function_call()

◆ get_call()

◆ goto_inline() [1/3]

◆ goto_inline() [2/3]

◆ goto_inline() [3/3]

◆ goto_inline_nontransitive()

◆ goto_inline_transitive()

◆ insert_function_body()

◆ is_ignored()

◆ output_cache()

◆ output_inline_log_json()

◆ output_inline_map()

◆ parameter_assignments()

◆ parameter_destruction()

◆ replace_return()

Member Data Documentation

◆ adjust_function

◆ cache

◆ caching

◆ finished_set

◆ goto_functions

◆ inline_log

◆ log

◆ no_body_set

◆ ns

◆ recursion_set