CBMC
remove_exceptions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove function exceptional returns
4 
5 Author: Cristina David
6 
7 Date: 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 
19 class class_hierarchyt;
20 class goto_modelt;
21 class goto_programt;
22 class message_handlert;
23 class 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 
32 void remove_exceptions_using_instanceof(
33  const irep_idt &function_identifier,
34  goto_programt &,
35  symbol_table_baset &,
36  message_handlert &);
37 
41 void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &);
42 
46 void remove_exceptions(
47  const irep_idt &function_identifier,
48  goto_programt &,
49  symbol_table_baset &,
50  const class_hierarchyt &,
51  message_handlert &);
52 
56 void 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:28
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