cprover
|
Remove function returns. More...
#include <goto-programs/goto_model.h>
Go to the source code of this file.
Macros | |
#define | RETURN_VALUE_SUFFIX "#return_value" |
Functions | |
void | remove_returns (symbol_tablet &, goto_functionst &) |
removes returns More... | |
void | remove_returns (goto_modelt &) |
removes returns More... | |
void | restore_returns (symbol_tablet &, goto_functionst &) |
restores return statements More... | |
code_typet | original_return_type (const symbol_tablet &symbol_table, const irep_idt &function_id) |
Remove function returns.
Definition in file remove_returns.h.
#define RETURN_VALUE_SUFFIX "#return_value" |
Definition at line 19 of file remove_returns.h.
Referenced by remove_returnst::do_function_calls(), mm_io(), original_return_type(), remove_returnst::replace_returns(), remove_returnst::restore_returns(), and remove_returnst::undo_function_calls().
code_typet original_return_type | ( | const symbol_tablet & | symbol_table, |
const irep_idt & | function_id | ||
) |
Definition at line 217 of file remove_returns.cpp.
References id2string(), irept::make_nil(), RETURN_VALUE_SUFFIX, symbol_tablet::symbols, and to_code_type().
Referenced by goto_program_coverage_recordt::goto_program_coverage_recordt(), and remove_returnst::restore_returns().
void remove_returns | ( | symbol_tablet & | , |
goto_functionst & | |||
) |
removes returns
Definition at line 202 of file remove_returns.cpp.
Referenced by goto_instrument_parse_optionst::do_remove_returns(), goto_diff_parse_optionst::doit(), goto_instrument_parse_optionst::instrument_goto_program(), goto_diff_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
void remove_returns | ( | goto_modelt & | ) |
removes returns
Definition at line 211 of file remove_returns.cpp.
References goto_modelt::goto_functions, and goto_modelt::symbol_table.
void restore_returns | ( | symbol_tablet & | , |
goto_functionst & | |||
) |
restores return statements
Definition at line 392 of file remove_returns.cpp.
References remove_returnst::restore().
Referenced by goto_instrument_parse_optionst::doit().