|
cprover
|
Remove function returns. More...
Include dependency graph for remove_returns.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Macros | |
| #define | RETURN_VALUE_SUFFIX "#return_value" |
Typedefs | |
| typedef std::function< bool(const irep_idt &)> | function_is_stubt |
Functions | |
| void | remove_returns (symbol_table_baset &, goto_functionst &) |
| removes returns More... | |
| void | remove_returns (goto_model_functiont &, function_is_stubt) |
| Removes returns from a single function. More... | |
| void | remove_returns (goto_modelt &) |
| removes returns More... | |
| void | restore_returns (symbol_table_baset &, goto_functionst &) |
| void | restore_returns (goto_modelt &) |
| restores return statements More... | |
| code_typet | original_return_type (const symbol_table_baset &symbol_table, const irep_idt &function_id) |
| Get code type of a function that has had remove_returns run upon it. More... | |
Remove function returns.
Definition in file remove_returns.h.
| #define RETURN_VALUE_SUFFIX "#return_value" |
Definition at line 21 of file remove_returns.h.
| typedef std::function<bool(const irep_idt &)> function_is_stubt |
Definition at line 34 of file remove_returns.h.
| code_typet original_return_type | ( | const symbol_table_baset & | symbol_table, |
| const irep_idt & | function_id | ||
| ) |
Get code type of a function that has had remove_returns run upon it.
| symbol_table | global symbol table |
| function_id | function to get the type of |
return_type() restored to its original value Definition at line 300 of file remove_returns.cpp.
| void remove_returns | ( | symbol_table_baset & | , |
| goto_functionst & | |||
| ) |
removes returns
Definition at line 261 of file remove_returns.cpp.
| void remove_returns | ( | goto_model_functiont & | goto_model_function, |
| function_is_stubt | function_is_stub | ||
| ) |
Removes returns from a single function.
Only usable with Java programs at the moment; to use it with other languages, they must annotate their stub functions with ID_C_incomplete as currently done in java_bytecode_convert_method.cpp.
This will generate #return_value variables, if not already present, for both the function being altered and any callees.
| goto_model_function | function to transform |
| function_is_stub | function that will be used to test whether a given callee has been or will be given a body. It should return true if so, or false if the function will remain a bodyless stub. |
Definition at line 280 of file remove_returns.cpp.
| void remove_returns | ( | goto_modelt & | ) |
removes returns
Definition at line 289 of file remove_returns.cpp.
| void restore_returns | ( | symbol_table_baset & | , |
| goto_functionst & | |||
| ) |
| void restore_returns | ( | goto_modelt & | ) |
restores return statements
Definition at line 449 of file remove_returns.cpp.