Replace function returns by assignments to global variables. More...
#include "remove_returns.h"#include <util/std_code.h>#include <util/std_expr.h>#include <util/suffix.h>#include <goto-symex/shadow_memory.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 |
Macros | |
| #define | RETURN_VALUE_SUFFIX "#return_value" |
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... | |
| void | restore_returns (goto_modelt &goto_model) |
| restores return statements More... | |
| irep_idt | return_value_identifier (const irep_idt &identifier) |
| produces the identifier that is used to store the return value of the function with the given identifier More... | |
| symbol_exprt | return_value_symbol (const irep_idt &identifier, const namespacet &ns) |
| produces the symbol that is used to store the return value of the function with the given identifier More... | |
| bool | is_return_value_identifier (const irep_idt &id) |
Returns true if id is a special return-value symbol produced by return_value_identifier. More... | |
| bool | is_return_value_symbol (const symbol_exprt &symbol_expr) |
Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol. More... | |
| bool | does_function_call_return (const goto_programt::instructiont &function_call) |
Check if the function_call returns anything. More... | |
Detailed Description
Replace function returns by assignments to global variables.
Definition in file remove_returns.cpp.
Macro Definition Documentation
◆ RETURN_VALUE_SUFFIX
| #define RETURN_VALUE_SUFFIX "#return_value" |
Definition at line 25 of file remove_returns.cpp.
Function Documentation
◆ does_function_call_return()
| bool does_function_call_return | ( | const goto_programt::instructiont & | function_call | ) |
Check if the function_call returns anything.
- Parameters
-
function_call the function call to be investigated
- Returns
- true if non-void return type and non-nil lhs
Definition at line 430 of file remove_returns.cpp.
◆ is_return_value_identifier()
| bool is_return_value_identifier | ( | const irep_idt & | id | ) |
Returns true if id is a special return-value symbol produced by return_value_identifier.
Definition at line 420 of file remove_returns.cpp.
◆ is_return_value_symbol()
| bool is_return_value_symbol | ( | const symbol_exprt & | symbol_expr | ) |
Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol.
Definition at line 425 of file remove_returns.cpp.
◆ remove_returns() [1/3]
| 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.
- Parameters
-
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 278 of file remove_returns.cpp.
◆ remove_returns() [2/3]
| void remove_returns | ( | goto_modelt & | goto_model | ) |
removes returns
Definition at line 287 of file remove_returns.cpp.
◆ remove_returns() [3/3]
| void remove_returns | ( | symbol_table_baset & | symbol_table, |
| goto_functionst & | goto_functions | ||
| ) |
removes returns
Definition at line 259 of file remove_returns.cpp.
◆ restore_returns()
| void restore_returns | ( | goto_modelt & | goto_model | ) |
restores return statements
Definition at line 401 of file remove_returns.cpp.
◆ return_value_identifier()
produces the identifier that is used to store the return value of the function with the given identifier
Definition at line 407 of file remove_returns.cpp.
◆ return_value_symbol()
| symbol_exprt return_value_symbol | ( | const irep_idt & | identifier, |
| const namespacet & | ns | ||
| ) |
produces the symbol that is used to store the return value of the function with the given identifier
Definition at line 413 of file remove_returns.cpp.
