Go to the documentation of this file.
71 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
72 #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
120 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
std::function< bool(const irep_idt &)> function_is_stubt
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
codet representation of a function call statement.
The symbol table base class interface.
bool is_return_value_identifier(const irep_idt &id)
Returns true if id is a special return-value symbol produced by return_value_identifier.
void remove_returns(symbol_table_baset &, goto_functionst &)
removes returns
A collection of goto functions.
void restore_returns(symbol_table_baset &, goto_functionst &)
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
Interface providing access to a single function in a GOTO model, plus its associated symbol table.