Remove function returns. More...

#include <functional>
#include <util/std_types.h>

Include dependency graph for remove_returns.h:

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

Macros
#define	RETURN_VALUE_SUFFIX "#return_value"

Typedefs
typedef std::function< bool(const irep_idt &)>	function_is_stubt

Functions
void	remove_returns (symbol_table_baset &, goto_functionst &)
	removes returns More...

void	remove_returns (goto_model_functiont &, function_is_stubt)
	Removes returns from a single function. More...

void	remove_returns (goto_modelt &)
	removes returns More...

void	restore_returns (symbol_table_baset &, goto_functionst &)

void	restore_returns (goto_modelt &)
	restores return statements More...

code_typet	original_return_type (const symbol_table_baset &symbol_table, const irep_idt &function_id)
	Get code type of a function that has had remove_returns run upon it. More...

Detailed Description

Remove function returns.

Definition in file remove_returns.h.

Macro Definition Documentation

◆ RETURN_VALUE_SUFFIX

#define RETURN_VALUE_SUFFIX "#return_value"

Definition at line 21 of file remove_returns.h.

Referenced by remove_returnst::get_or_create_return_value_symbol(), mm_io(), replace_callst::operator()(), original_return_type(), remove_returnst::restore_returns(), and remove_returnst::undo_function_calls().

Typedef Documentation

◆ function_is_stubt

typedef std::function<bool(const irep_idt &)> function_is_stubt

Definition at line 34 of file remove_returns.h.

Function Documentation

◆ original_return_type()

code_typet original_return_type	(	const symbol_table_baset &	symbol_table,
		const irep_idt &	function_id
	)

Get code type of a function that has had remove_returns run upon it.

Parameters

symbol_table	global symbol table
function_id	function to get the type of

Returns: the function's type with its return_type() restored to its original value

Definition at line 294 of file remove_returns.cpp.

References id2string(), symbol_table_baset::lookup_ref(), code_typet::return_type(), RETURN_VALUE_SUFFIX, symbol_table_baset::symbols, to_code_type(), and symbolt::type.

Referenced by goto_program_coverage_recordt::goto_program_coverage_recordt(), and remove_returnst::restore_returns().

◆ remove_returns() [1/3]

void remove_returns	(	symbol_table_baset &	,
		goto_functionst &
	)

removes returns

Definition at line 255 of file remove_returns.cpp.

Referenced by goto_instrument_parse_optionst::do_remove_returns(), jbmc_parse_optionst::process_goto_function(), goto_diff_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), and goto_analyzer_parse_optionst::process_goto_program().

◆ remove_returns() [2/3]

void remove_returns	(	goto_model_functiont &	goto_model_function,
		function_is_stubt	function_is_stub
	)

Removes returns from a single function.

Only usable with Java programs at the moment; to use it with other languages, they must annotate their stub functions with ID_C_incomplete as currently done in java_bytecode_convert_method.cpp.

This will generate #return_value variables, if not already present, for both the function being altered and any callees.

Parameters

goto_model_function	function to transform
function_is_stub	function that will be used to test whether a given callee has been or will be given a body. It should return true if so, or false if the function will remain a bodyless stub.

Definition at line 274 of file remove_returns.cpp.

References goto_model_functiont::get_symbol_table().

◆ remove_returns() [3/3]

void remove_returns ( goto_modelt & )

removes returns

Definition at line 283 of file remove_returns.cpp.

References goto_modelt::goto_functions, and goto_modelt::symbol_table.

◆ restore_returns() [1/2]

void restore_returns	(	symbol_table_baset &	,
		goto_functionst &
	)

◆ restore_returns() [2/2]

void restore_returns ( goto_modelt & )

restores return statements

Definition at line 443 of file remove_returns.cpp.

References goto_modelt::goto_functions, remove_returnst::restore(), and goto_modelt::symbol_table.

Referenced by goto_instrument_parse_optionst::doit(), and static_simplifier().

Macros

Typedefs

Functions