cprover
remove_returns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove function returns
4 
5 Author: Daniel Kroening
6 
7 Date: September 2009
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
15 #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
16 
18 
19 #define RETURN_VALUE_SUFFIX "#return_value"
20 
21 // Turns 'return x' into an assignment to fkt#return_value,
22 // unless the function returns void,
23 // and a 'goto the_end_of_the_function'.
24 
26 
28 
29 // reverse the above operations
31 
33  const symbol_tablet &symbol_table,
34  const irep_idt &function_id);
35 
36 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
Base type of functions.
Definition: std_types.h:734
void restore_returns(symbol_tablet &, goto_functionst &)
restores return statements
code_typet original_return_type(const symbol_tablet &symbol_table, const irep_idt &function_id)
Symbol Table + CFG.
void remove_returns(symbol_tablet &, goto_functionst &)
removes returns
The symbol table.
Definition: symbol_table.h:52