cprover
remove_returns.h File Reference

Replace function returns by assignments to global variables. 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:

Go to the source code of this file.

Macros

#define RETURN_VALUE_SUFFIX   "#return_value"
 The functions remove_returns() remove return instructions from a goto program. More...
 

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

Detailed Description

Replace function returns by assignments to global variables.

Definition in file remove_returns.h.

Macro Definition Documentation

◆ RETURN_VALUE_SUFFIX

#define RETURN_VALUE_SUFFIX   "#return_value"

The functions remove_returns() remove return instructions from a goto program.

The restore_returns() functions restore the returns in a goto program in which they have been removed previously.

In a goto program in which returns have not been removed, functions return values via the return instruction, which is followed by a GOTO to the end of the function. Unlike in C, in a goto program the return instruction does not cause control-flow to return to the call site. Instead, it simply sets the return value that will be returned once the function returns to the call site when the END_FUNCTION instruction is encountered.

Consider the following C code (with ... indicating further code):

int func()
{
...
return 1;
...
}
r = func();

This code would appear in a goto program as follows:

func
...
return 1;
GOTO 1
...
r = func();

The return removal pass introduces a thread-local global variable func::return_value (one for each non-void function) to which the return value is assigned, and this variable is then assigned to the lhs expression that takes the function return value:

func
...
func#return_value = 1;
GOTO 1
...
func();
r = func#return_value;

remove_returns() does not change the signature of the function.

Definition at line 78 of file remove_returns.h.

Typedef Documentation

◆ function_is_stubt

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

Definition at line 87 of file remove_returns.h.

Function Documentation

◆ remove_returns() [1/3]

void remove_returns ( symbol_table_baset ,
goto_functionst  
)

removes returns

Definition at line 254 of file remove_returns.cpp.

◆ 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_functionfunction to transform
function_is_stubfunction 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 273 of file remove_returns.cpp.

◆ remove_returns() [3/3]

void remove_returns ( goto_modelt )

removes returns

Definition at line 282 of file remove_returns.cpp.

◆ 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 407 of file remove_returns.cpp.