#include <util/irep.h>
#include <functional>
#include "goto_function.h"

Include dependency graph for remove_returns.h:

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

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...

irep_idt	return_value_identifier (const irep_idt &)
	produces the identifier that is used to store the return value of the function with the given identifier More...

symbol_exprt	return_value_symbol (const irep_idt &, const namespacet &)
	produces the symbol that is used to store the return value of the function with the given identifier More...

bool	is_return_value_identifier (const irep_idt &id)
	Returns true if `id` is a special return-value symbol produced by return_value_identifier. More...

bool	is_return_value_symbol (const symbol_exprt &symbol_expr)
	Returns true if `symbol_expr` is a special return-value symbol produced by return_value_symbol. More...

bool	does_function_call_return (const goto_programt::instructiont &function_call)
	Check if the `function_call` returns anything. More...

Detailed Description

Replace function returns by assignments to global variables

Definition in file remove_returns.h.

Typedef Documentation

◆ function_is_stubt

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

Definition at line 90 of file remove_returns.h.

Function Documentation

◆ does_function_call_return()

bool does_function_call_return ( const goto_programt::instructiont & function_call )

Check if the function_call returns anything.

Parameters

function_call the function call to be investigated

Returns: true if non-void return type and non-nil lhs

Definition at line 426 of file remove_returns.cpp.

◆ is_return_value_identifier()

bool is_return_value_identifier ( const irep_idt & id )

Returns true if id is a special return-value symbol produced by return_value_identifier.

Definition at line 416 of file remove_returns.cpp.

◆ is_return_value_symbol()

bool is_return_value_symbol ( const symbol_exprt & symbol_expr )

Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol.

Definition at line 421 of file remove_returns.cpp.

◆ remove_returns() [1/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.

◆ remove_returns() [2/3]

void remove_returns ( goto_modelt & )

removes returns

Definition at line 283 of file remove_returns.cpp.

◆ remove_returns() [3/3]

void remove_returns	(	symbol_table_baset &	,
		goto_functionst &
	)

removes returns

Definition at line 255 of file remove_returns.cpp.

◆ restore_returns() [1/2]

void restore_returns ( goto_modelt & )

restores return statements

Definition at line 397 of file remove_returns.cpp.

◆ restore_returns() [2/2]

void restore_returns	(	symbol_table_baset &	,
		goto_functionst &
	)

◆ return_value_identifier()

irep_idt return_value_identifier ( const irep_idt & )

produces the identifier that is used to store the return value of the function with the given identifier

Definition at line 403 of file remove_returns.cpp.

◆ return_value_symbol()

symbol_exprt return_value_symbol	(	const irep_idt &	,
		const namespacet &
	)

produces the symbol that is used to store the return value of the function with the given identifier

Definition at line 409 of file remove_returns.cpp.

Typedefs

Functions