cprover
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 
19 
20 #include <util/message.h>
21 
22 #define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"
23 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \
24  "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
25 
30  const irep_idt &function_identifier,
31  goto_programt &,
34 
39 
44  const irep_idt &function_identifier,
45  goto_programt &,
47  const class_hierarchyt &,
49 
54  goto_modelt &,
55  const class_hierarchyt &,
57 
58 #endif
Class Hierarchy.
Non-graph-based representation of the class hierarchy.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
The symbol table base class interface.
Symbol Table + CFG.
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...
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...