CBMC
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...
 
bool 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 (const irep_idt &function_id, goto_programt &goto_program)
 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...
 
std::optional< symbol_exprtget_or_create_return_value_symbol (const irep_idt &function_id)
 

Protected Attributes

symbol_table_basetsymbol_table
 

Detailed Description

Definition at line 27 of file remove_returns.cpp.

Constructor & Destructor Documentation

◆ remove_returnst()

remove_returnst::remove_returnst ( symbol_table_baset _symbol_table)
inlineexplicit

Definition at line 30 of file remove_returns.cpp.

Member Function Documentation

◆ do_function_calls()

bool 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
Returns
True if, and only if, instructions have been inserted. In that case the caller must invoke an appropriate method to update location numbers.

Definition at line 149 of file remove_returns.cpp.

◆ get_or_create_return_value_symbol()

std::optional< symbol_exprt > remove_returnst::get_or_create_return_value_symbol ( const irep_idt function_id)
protected

Definition at line 67 of file remove_returns.cpp.

◆ operator()() [1/2]

void remove_returnst::operator() ( goto_functionst goto_functions)

Definition at line 218 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 241 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 102 of file remove_returns.cpp.

◆ restore()

void remove_returnst::restore ( goto_functionst goto_functions)

Definition at line 383 of file remove_returns.cpp.

◆ restore_returns()

bool remove_returnst::restore_returns ( const irep_idt function_id,
goto_programt goto_program 
)
protected

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

Definition at line 294 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 337 of file remove_returns.cpp.

Member Data Documentation

◆ symbol_table

symbol_table_baset& remove_returnst::symbol_table
protected

Definition at line 46 of file remove_returns.cpp.


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