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 
18 
19 #include <util/message.h>
20 
21 #define INFLIGHT_EXCEPTION_VARIABLE_BASENAME "@inflight_exception"
22 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \
23  "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME
24 
25 // Removes 'throw x' and CATCH-PUSH/CATCH-POP
26 // and adds the required instrumentation (GOTOs and assignments)
27 
29 {
32 };
33 
36  symbol_table_baset &symbol_table,
40 
42  goto_modelt &goto_model,
46 
47 #endif
remove_exceptions_typest
Symbol Table + CFG.
void remove_exceptions(goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, remove_exceptions_typest type=remove_exceptions_typest::DONT_REMOVE_INSTANCEOF)
removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing them with explicit exceptio...
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
The symbol table base class interface.
goto_programt & goto_program
Definition: cover.cpp:63
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66