cprover
|
#include "remove_returns.h"
#include <util/std_expr.h>
#include "goto_model.h"
#include "remove_skip.h"
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 | ( | 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 remove_returns | ( | symbol_table_baset & | symbol_table, |
goto_functionst & | goto_functions | ||
) |
removes returns
Definition at line 261 of file remove_returns.cpp.
void restore_returns | ( | goto_modelt & | goto_model | ) |
restores return statements
Definition at line 449 of file remove_returns.cpp.