cprover
Loading...
Searching...
No Matches
java_bytecode_instrument.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument codet with assertions/runtime exceptions
4
5Author: Cristina David
6
7Date: 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
17class code_blockt;
20class symbol_tablet;
21class symbolt;
23
25 symbol_table_baset &symbol_table,
26 symbolt &symbol,
27 const bool throw_runtime_exceptions,
28 message_handlert &_message_handler);
29
31 symbol_tablet &symbol_table,
32 const bool throw_runtime_exceptions,
33 message_handlert &_message_handler);
34
36 code_blockt &init_code,
37 const symbolt &exc_symbol,
38 const source_locationt &source_location);
39
40extern const std::vector<std::string> exception_needed_classes;
41
42#endif
A codet representing sequential composition of program statements.
Definition: std_code.h:130
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
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...
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.
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.
const std::vector< std::string > exception_needed_classes