|
CBMC
|
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... | |
| 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.