CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
remove_exceptions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove function exceptional returns
4
5Author: Cristina David
6
7Date: December 2016
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
15#define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
16
17#include <util/irep.h>
18
19class class_hierarchyt;
20class goto_modelt;
21class goto_programt;
22class message_handlert;
23class symbol_table_baset;
24
25#define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"
26#define INFLIGHT_EXCEPTION_VARIABLE_NAME \
27 "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
28
32void remove_exceptions_using_instanceof(
33 const irep_idt &function_identifier,
34 goto_programt &,
35 symbol_table_baset &,
36 message_handlert &);
37
41void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &);
42
46void remove_exceptions(
47 const irep_idt &function_identifier,
48 goto_programt &,
49 symbol_table_baset &,
50 const class_hierarchyt &,
51 message_handlert &);
52
56void remove_exceptions(
57 goto_modelt &,
58 const class_hierarchyt &,
59 message_handlert &);
60
61#endif
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition class_hierarchy.h:41
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
goto_modelt
Definition goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:73
message_handlert
Definition message.h:27
symbol_table_baset
The symbol table base class interface.
Definition symbol_table_base.h:23
remove_exceptions
void remove_exceptions(const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, const class_hierarchyt &, message_handlert &)
Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignmen...
Definition remove_exceptions.cpp:723
remove_exceptions_using_instanceof
void remove_exceptions_using_instanceof(const irep_idt &function_identifier, goto_programt &, symbol_table_baset &, message_handlert &)
Removes 'throw x' and CATCH-PUSH/CATCH-POP and adds the required instrumentation (GOTOs and assignmen...
Definition remove_exceptions.cpp:656