11 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H 12 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H 23 const bool throw_runtime_exceptions,
28 const bool throw_runtime_exceptions,
const std::vector< std::string > exception_needed_classes
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
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...
A codet representing sequential composition of program statements.