cprover
remove_returns.cpp File Reference

Remove function return values. More...

#include "remove_returns.h"
#include <util/std_expr.h>
#include "goto_model.h"
#include "remove_skip.h"
Include dependency graph for remove_returns.cpp:

Go to the source code of this file.

Classes

class  remove_returnst
 

Functions

void remove_returns (symbol_table_baset &symbol_table, goto_functionst &goto_functions)
 removes returns More...
 
void remove_returns (goto_model_functiont &goto_model_function, function_is_stubt function_is_stub)
 Removes returns from a single function. More...
 
void remove_returns (goto_modelt &goto_model)
 removes returns 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...
 
void restore_returns (goto_modelt &goto_model)
 restores return statements More...
 

Detailed Description

Remove function return values.

Definition in file remove_returns.cpp.

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_tableglobal symbol table
function_idfunction 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]

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

References goto_model_functiont::get_symbol_table().

◆ remove_returns() [3/3]

void remove_returns ( goto_modelt goto_model)

removes returns

Definition at line 283 of file remove_returns.cpp.

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

◆ restore_returns()

void restore_returns ( goto_modelt goto_model)