remove_exceptions.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Remove function exceptional returns
 
Author: Cristina David
 
Date:   December 2016
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
#define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 
#include <util/irep.h>
 
class class_hierarchyt;
class goto_modelt;
class goto_programt;
class message_handlert;
class symbol_table_baset;
 
#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"
#define INFLIGHT_EXCEPTION_VARIABLE_NAME \
  "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
 
void remove_exceptions_using_instanceof(
  const irep_idt &function_identifier,
  goto_programt &,
  symbol_table_baset &,
  message_handlert &);
 
void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &);
 
void remove_exceptions(
  const irep_idt &function_identifier,
  goto_programt &,
  symbol_table_baset &,
  const class_hierarchyt &,
  message_handlert &);
 
void remove_exceptions(
  goto_modelt &,
  const class_hierarchyt &,
  message_handlert &);
 
#endif