cprover
remove_returnst Class Reference
Collaboration diagram for remove_returnst:
[legend]

Public Member Functions

 remove_returnst (symbol_table_baset &_symbol_table)
 
void operator() (goto_functionst &goto_functions)
 
void operator() (goto_model_functiont &model_function, function_is_stubt function_is_stub)
 
void restore (goto_functionst &goto_functions)
 

Protected Member Functions

void replace_returns (const irep_idt &function_id, goto_functionst::goto_functiont &function)
 turns 'return x' into an assignment to fkt::return_value More...
 
void do_function_calls (function_is_stubt function_is_stub, goto_programt &goto_program)
 turns x=f(...) into f(...); lhs=f::return_value; More...
 
bool restore_returns (goto_functionst::function_mapt::iterator f_it)
 turns an assignment to fkt::return_value back into 'return x' More...
 
void undo_function_calls (goto_functionst &goto_functions, goto_programt &goto_program)
 turns f(...); lhs=f::return_value; into lhs=f(...) More...
 
symbol_exprt get_or_create_return_value_symbol (const irep_idt &function_id)
 

Protected Attributes

symbol_table_basetsymbol_table
 

Detailed Description

Definition at line 22 of file remove_returns.cpp.

Constructor & Destructor Documentation

◆ remove_returnst()

remove_returnst::remove_returnst ( symbol_table_baset _symbol_table)
inlineexplicit

Definition at line 25 of file remove_returns.cpp.

Member Function Documentation

◆ do_function_calls()

void remove_returnst::do_function_calls ( function_is_stubt  function_is_stub,
goto_programt goto_program 
)
protected

turns x=f(...) into f(...); lhs=f::return_value;

Parameters
function_is_stubfunction (irep_idt -> bool) that determines whether a given function ID is a stub
goto_programprogram to transform

Definition at line 139 of file remove_returns.cpp.

References Forall_goto_program_instructions, code_function_callt::function(), get_or_create_return_value_symbol(), goto_program, irept::id(), goto_programt::insert_after(), INVARIANT, irept::is_not_nil(), code_function_callt::lhs(), irept::make_nil(), to_code_function_call(), to_code_type(), to_symbol_expr(), and exprt::type().

Referenced by operator()().

◆ get_or_create_return_value_symbol()

◆ operator()() [1/2]

void remove_returnst::operator() ( goto_functionst goto_functions)

◆ operator()() [2/2]

void remove_returnst::operator() ( goto_model_functiont model_function,
function_is_stubt  function_is_stub 
)

◆ replace_returns()

void remove_returnst::replace_returns ( const irep_idt function_id,
goto_functionst::goto_functiont function 
)
protected

turns 'return x' into an assignment to fkt::return_value

Parameters
function_idname of the function to transform
functionfunction to transform

Definition at line 96 of file remove_returns.cpp.

References Forall_goto_program_instructions, get_or_create_return_value_symbol(), symbol_table_baset::get_writeable(), goto_program, INVARIANT, exprt::op0(), symbol_table, and symbolt::type.

Referenced by operator()().

◆ restore()

void remove_returnst::restore ( goto_functionst goto_functions)

Definition at line 429 of file remove_returns.cpp.

References Forall_goto_functions, restore_returns(), and undo_function_calls().

Referenced by restore_returns().

◆ restore_returns()

bool remove_returnst::restore_returns ( goto_functionst::function_mapt::iterator  f_it)
protected

◆ undo_function_calls()

Member Data Documentation

◆ symbol_table

symbol_table_baset& remove_returnst::symbol_table
protected

The documentation for this class was generated from the following file: