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 codet;
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  codet &init_code,
33  const symbolt &exc_symbol,
35 
36 extern const std::vector<std::string> exception_needed_classes;
37 
38 #endif
void java_bytecode_instrument_uncaught_exceptions(codet &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...
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
const std::vector< std::string > exception_needed_classes
The symbol table.
Definition: symbol_table.h:19
Author: Diffblue Ltd.
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...
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.
The symbol table base class interface.
const source_locationt & source_location() const
Definition: expr.h:125
A statement in a programming language.
Definition: std_code.h:21