cprover
remove_returns.h File Reference

Remove function returns. More...

Include dependency graph for remove_returns.h:
This graph shows which files directly or indirectly include this file:

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)
 

Detailed Description

Remove function returns.

Definition in file remove_returns.h.

Macro Definition Documentation

§ RETURN_VALUE_SUFFIX

Function Documentation

§ original_return_type()

code_typet original_return_type ( const symbol_tablet symbol_table,
const irep_idt function_id 
)

§ remove_returns() [1/2]

§ remove_returns() [2/2]

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.

§ restore_returns()

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().