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 
70 
71 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
72 #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
73 
74 #include <functional>
75 
76 #include <util/std_code.h>
77 #include <util/std_types.h>
78 
79 class goto_functionst;
81 class goto_modelt;
82 class namespacet;
83 class symbol_table_baset;
84 class symbol_exprt;
85 
87 
88 typedef std::function<bool(const irep_idt &)> function_is_stubt;
89 
91 
93 
94 // reverse the above operations
96 
98 
102 
106 
109 bool is_return_value_identifier(const irep_idt &id);
110 
113 bool is_return_value_symbol(const symbol_exprt &symbol_expr);
114 
118 bool does_function_call_return(const code_function_callt &function_call);
119 
120 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
return_value_identifier
irep_idt return_value_identifier(const irep_idt &)
produces the identifier that is used to store the return value of the function with the given identif...
Definition: remove_returns.cpp:409
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
does_function_call_return
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
Definition: remove_returns.cpp:432
goto_modelt
Definition: goto_model.h:26
function_is_stubt
std::function< bool(const irep_idt &)> function_is_stubt
Definition: remove_returns.h:88
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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: remove_returns.cpp:427
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_types.h
Pre-defined types.
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: remove_returns.cpp:422
std_code.h
remove_returns
void remove_returns(symbol_table_baset &, goto_functionst &)
removes returns
Definition: remove_returns.cpp:256
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
restore_returns
void restore_returns(symbol_table_baset &, goto_functionst &)
return_value_symbol
symbol_exprt return_value_symbol(const irep_idt &, const namespacet &)
produces the symbol that is used to store the return value of the function with the given identifier
Definition: remove_returns.cpp:415
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183