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 
17 #include <functional>
18 
19 #include <util/std_types.h>
20 
21 #define RETURN_VALUE_SUFFIX "#return_value"
22 
23 class goto_functionst;
25 class goto_modelt;
26 class symbol_table_baset;
27 
28 // Turns 'return x' into an assignment to fkt#return_value,
29 // unless the function returns void,
30 // and a 'goto the_end_of_the_function'.
31 
33 
34 typedef std::function<bool(const irep_idt &)> function_is_stubt;
35 
37 
39 
40 // reverse the above operations
42 
44 
46  const symbol_table_baset &symbol_table,
47  const irep_idt &function_id);
48 
49 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
std::function< bool(const irep_idt &)> function_is_stubt
Base type of functions.
Definition: std_types.h:751
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Pre-defined types.
The symbol table base class interface.
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.
void remove_returns(symbol_table_baset &, goto_functionst &)
removes returns
void restore_returns(symbol_table_baset &, goto_functionst &)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:153