|
cprover
|
Remove function return values. More...
#include "remove_returns.h"#include <util/std_expr.h>#include "goto_model.h"#include "remove_skip.h"
Include dependency graph for remove_returns.cpp:Go to the source code of this file.
Classes | |
| class | remove_returnst |
Functions | |
| void | remove_returns (symbol_table_baset &symbol_table, goto_functionst &goto_functions) |
| removes returns More... | |
| void | remove_returns (goto_model_functiont &goto_model_function, function_is_stubt function_is_stub) |
| Removes returns from a single function. More... | |
| void | remove_returns (goto_modelt &goto_model) |
| removes returns 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... | |
| void | restore_returns (goto_modelt &goto_model) |
| restores return statements More... | |
Remove function return values.
Definition in file remove_returns.cpp.
| 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 & | symbol_table, |
| goto_functionst & | goto_functions | ||
| ) |
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 & | goto_model | ) |
removes returns
Definition at line 289 of file remove_returns.cpp.
| void restore_returns | ( | goto_modelt & | goto_model | ) |
restores return statements
Definition at line 449 of file remove_returns.cpp.