cprover
java_bytecode_instrument.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrument codet with assertions/runtime exceptions
4 
5 Author: Cristina David
6 
7 Date: June 2017
8 
9 \*******************************************************************/
10 
11 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
12 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
13 
14 #include <util/symbol_table.h>
15 #include <util/message.h>
16 #include <util/irep.h>
17 
18 class code_blockt;
19 
21  symbol_table_baset &symbol_table,
22  symbolt &symbol,
23  const bool throw_runtime_exceptions,
24  message_handlert &_message_handler);
25 
27  symbol_tablet &symbol_table,
28  const bool throw_runtime_exceptions,
29  message_handlert &_message_handler);
30 
32  code_blockt &init_code,
33  const symbolt &exc_symbol,
35 
36 extern const std::vector<std::string> exception_needed_classes;
37 
38 #endif
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
exception_needed_classes
const std::vector< std::string > exception_needed_classes
Definition: java_bytecode_instrument.cpp:79
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_bytecode_instrument_symbol
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &_message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
Definition: java_bytecode_instrument.cpp:545
message_handlert
Definition: message.h:28
source_locationt
Definition: source_location.h:20
java_bytecode_instrument_uncaught_exceptions
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
Definition: java_bytecode_instrument.cpp:568
symbolt
Symbol table entry.
Definition: symbol.h:28
java_bytecode_instrument
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &_message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
Definition: java_bytecode_instrument.cpp:595
symbol_table.h
Author: Diffblue Ltd.
message.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
irep.h