CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
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
 
bool  do_function_calls (function_is_stubt function_is_stub, goto_programt &goto_program)
  turns x=f(...) into f(...); lhs=f::return_value;
 
bool  restore_returns (const irep_idt &function_id, goto_programt &goto_program)
  turns an assignment to fkt::return_value back into 'return x'
 
void  undo_function_calls (goto_programt &goto_program)
  turns f(...); lhs=f::return_value; into lhs=f(...)
 
std::optional< symbol_exprt >  get_or_create_return_value_symbol (const irep_idt &function_id)
 

Protected Attributes

symbol_table_baset &  symbol_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_stub function (irep_idt -> bool) that determines whether a given function ID is a stub
goto_program program 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_id name of the function to transform
function function 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:

AltStyle によって変換されたページ (->オリジナル) /