CBMC
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 <string>
15 #include <vector>
16 
17 class code_blockt;
18 class message_handlert;
19 class symbol_table_baset;
20 class symbolt;
21 class source_locationt;
22 
23 void java_bytecode_instrument_symbol(
24  symbol_table_baset &symbol_table,
25  symbolt &symbol,
26  const bool throw_runtime_exceptions,
27  message_handlert &_message_handler);
28 
29 void java_bytecode_instrument(
30  symbol_table_baset &symbol_table,
31  const bool throw_runtime_exceptions,
32  message_handlert &_message_handler);
33 
34 void java_bytecode_instrument_uncaught_exceptions(
35  code_blockt &init_code,
36  const symbolt &exc_symbol,
37  const source_locationt &source_location);
38 
39 extern const std::vector<std::string> exception_needed_classes;
40 
41 #endif
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:130
message_handlert
Definition: message.h:28
source_locationt
Definition: source_location.h:20
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
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:567
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:544
java_bytecode_instrument
void java_bytecode_instrument(symbol_table_baset &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:594
exception_needed_classes
const std::vector< std::string > exception_needed_classes
Definition: java_bytecode_instrument.cpp:77