goto_inline.h File Reference

Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet. More...

#include <util/json.h>

Include dependency graph for goto_inline.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	goto_inline (goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function=false)
	Inline every function call into the entry_point() function. More...
void	goto_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false)
	Inline every function call into the entry_point() function. More...
void	goto_partial_inline (goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit=0, bool adjust_function=false)
	Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count). More...
void	goto_partial_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, unsigned smallfunc_limit=0, bool adjust_function=false)
	Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count). More...
void	goto_function_inline (goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
	Transitively inline all function calls made from a particular function. More...
void	goto_function_inline (goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
	Transitively inline all function calls made from a particular function. More...
jsont	goto_function_inline_and_log (goto_modelt &, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
void	goto_program_inline (goto_functionst &goto_functions, goto_programt &goto_program, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
	Transitively inline all function calls found in a particular program. More...

Detailed Description

Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet.

Definition in file goto_inline.h.

Function Documentation

goto_function_inline() [1/2]

void goto_function_inline	(	goto_functionst &	goto_functions,
		const irep_idt	function,
		const namespacet &	ns,
		message_handlert &	message_handler,
		bool	adjust_function,
		bool	caching
	)

Transitively inline all function calls made from a particular function.

Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_functions	The function map to use to find function bodies.
function	The function whose calls to inline.
ns	Namespace used by goto_inlinet.
message_handler	Message handler used by goto_inlinet.
adjust_function	Replace location in inlined function with call site.
caching	Tell goto_inlinet to cache.

Definition at line 264 of file goto_inline.cpp.

goto_function_inline() [2/2]

void goto_function_inline	(	goto_modelt &	goto_model,
		const irep_idt	function,
		message_handlert &	message_handler,
		bool	adjust_function,
		bool	caching
	)

Transitively inline all function calls made from a particular function.

Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_model	Source of the symbol table and function map to use.
function	The function whose calls to inline.
message_handler	Message handler used by goto_inlinet.
adjust_function	Replace location in inlined function with call site.
caching	Tell goto_inlinet to cache.

Definition at line 239 of file goto_inline.cpp.

goto_function_inline_and_log()

jsont goto_function_inline_and_log	(	goto_modelt &	goto_model,
		const irep_idt	function,
		message_handlert &	message_handler,
		bool	adjust_function = false,
		bool	caching = true
	)

Definition at line 308 of file goto_inline.cpp.

goto_inline() [1/2]

void goto_inline	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		message_handlert &	message_handler,
		bool	adjust_function
	)

Inline every function call into the entry_point() function.

Then delete the bodies of all of the other functions. This is pretty drastic and can result in a very large program. Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_functions	The function map to use.
ns	: The namespace to use.
message_handler	Message handler used by goto_inlinet.
adjust_function	Replace location in inlined function with call site.

Definition at line 47 of file goto_inline.cpp.

goto_inline() [2/2]

void goto_inline	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		bool	adjust_function
	)

Inline every function call into the entry_point() function.

Then delete the bodies of all of the other functions. This is pretty drastic and can result in a very large program. Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_model	Source of the symbol table and function map to use.
message_handler	Message handler used by goto_inlinet.
adjust_function	Replace location in inlined function with call site.

Definition at line 26 of file goto_inline.cpp.

goto_partial_inline() [1/2]

void goto_partial_inline	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		message_handlert &	message_handler,
		unsigned	smallfunc_limit,
		bool	adjust_function
	)

Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count).

Unlike the goto_inline functions, this doesn't remove function bodies after inlining. Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_functions	The function map to use to find functions containing calls and function bodies.
ns	Namespace used by goto_inlinet.
message_handler	Message handler used by goto_inlinet.
smallfunc_limit	The maximum number of instructions in functions to be inlined.
adjust_function	Replace location in inlined function with call site.

Definition at line 149 of file goto_inline.cpp.

goto_partial_inline() [2/2]

void goto_partial_inline	(	goto_modelt &	goto_model,
		message_handlert &	message_handler,
		unsigned	smallfunc_limit,
		bool	adjust_function
	)

Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count).

Unlike the goto_inline functions, this doesn't remove function bodies after inlining. Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_model	Source of the symbol table and function map to use.
message_handler	Message handler used by goto_inlinet.
smallfunc_limit	The maximum number of instructions in functions to be inlined.
adjust_function	Replace location in inlined function with call site.

Definition at line 122 of file goto_inline.cpp.

goto_program_inline()

void goto_program_inline	(	goto_functionst &	goto_functions,
		goto_programt &	goto_program,
		const namespacet &	ns,
		message_handlert &	message_handler,
		bool	adjust_function,
		bool	caching
	)

Transitively inline all function calls found in a particular program.

Caller is responsible for calling update(), compute_loop_numbers(), etc.

Parameters

goto_functions	The function map to use to find function bodies.
goto_program	The program whose calls to inline.
ns	Namespace used by goto_inlinet.
message_handler	Message handler used by goto_inlinet.
adjust_function	Replace location in inlined function with call site.
caching	Tell goto_inlinet to cache.

Definition at line 366 of file goto_inline.cpp.