CBMC
|
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... | |
optionalt< symbol_exprt > | get_or_create_return_value_symbol (const irep_idt &function_id) |
Protected Attributes | |
symbol_table_baset & | symbol_table |
Definition at line 26 of file remove_returns.cpp.
|
inlineexplicit |
Definition at line 29 of file remove_returns.cpp.
|
protected |
turns x=f(...) into f(...); lhs=f::return_value;
function_is_stub | function (irep_idt -> bool) that determines whether a given function ID is a stub |
goto_program | program to transform |
Definition at line 148 of file remove_returns.cpp.
|
protected |
Definition at line 66 of file remove_returns.cpp.
void remove_returnst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 217 of file remove_returns.cpp.
void remove_returnst::operator() | ( | goto_model_functiont & | model_function, |
function_is_stubt | function_is_stub | ||
) |
Definition at line 237 of file remove_returns.cpp.
|
protected |
turns 'return x' into an assignment to fkt::return_value
function_id | name of the function to transform |
function | function to transform |
Definition at line 101 of file remove_returns.cpp.
void remove_returnst::restore | ( | goto_functionst & | goto_functions | ) |
Definition at line 379 of file remove_returns.cpp.
|
protected |
turns an assignment to fkt::return_value back into 'return x'
Definition at line 290 of file remove_returns.cpp.
|
protected |
turns f(...); lhs=f::return_value; into lhs=f(...)
Definition at line 333 of file remove_returns.cpp.
|
protected |
Definition at line 45 of file remove_returns.cpp.