remove_returns.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Remove function returns
 
Author: Daniel Kroening
 
Date:   September 2009
 
\*******************************************************************/


 
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
#define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
 
#include <util/irep.h>
 
#include "goto_program.h"
 
#include <functional>
 
class goto_functionst;
class goto_model_functiont;
class goto_modelt;
class symbol_table_baset;
class symbol_exprt;
 
void remove_returns(symbol_table_baset &, goto_functionst &);
 
typedef std::function<bool(const irep_idt &)> function_is_stubt;
 
void remove_returns(goto_model_functiont &, function_is_stubt);
 
void remove_returns(goto_modelt &);
 
// reverse the above operations
void restore_returns(symbol_table_baset &, goto_functionst &);
 
void restore_returns(goto_modelt &);

irep_idt return_value_identifier(const irep_idt &);

symbol_exprt return_value_symbol(const irep_idt &, const namespacet &);

bool is_return_value_identifier(const irep_idt &id);

bool is_return_value_symbol(const symbol_exprt &symbol_expr);

bool does_function_call_return(
  const goto_programt::instructiont &function_call);
 
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H