cprover
|
Remove function returns. More...
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.