71#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
72#define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
This class represents an instruction in the GOTO intermediate representation.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
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.
bool does_function_call_return(const goto_programt::instructiont &function_call)
Check if the function_call returns anything.
void restore_returns(symbol_table_baset &, goto_functionst &)
std::function< bool(const irep_idt &)> function_is_stubt
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.
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
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...
void remove_returns(symbol_table_baset &, goto_functionst &)
removes returns
1.9.8