cprover
remove_returnst Class Reference
+ Collaboration diagram for remove_returnst:

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_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 138 of file remove_returns.cpp.

◆ get_or_create_return_value_symbol()

symbol_exprt remove_returnst::get_or_create_return_value_symbol ( const irep_idt function_id)
protected

Definition at line 61 of file remove_returns.cpp.

◆ operator()() [1/2]

void remove_returnst::operator() ( goto_functionst goto_functions)

Definition at line 226 of file remove_returns.cpp.

◆ operator()() [2/2]

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

Definition at line 244 of file remove_returns.cpp.

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

◆ restore()

void remove_returnst::restore ( goto_functionst goto_functions)

Definition at line 434 of file remove_returns.cpp.

◆ restore_returns()

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

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

Definition at line 321 of file remove_returns.cpp.

◆ undo_function_calls()

void remove_returnst::undo_function_calls ( goto_programt goto_program)
protected

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

Definition at line 374 of file remove_returns.cpp.

Member Data Documentation

◆ symbol_table

symbol_table_baset& remove_returnst::symbol_table
protected

Definition at line 41 of file remove_returns.cpp.


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