#include <string>
#include <vector>

Include dependency graph for java_bytecode_instrument.h:

This graph shows which files directly or indirectly include this file:

Functions
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. More...

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. More...

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 entry point. More...

Function Documentation

◆ 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.

Exceptions are thrown when the throw_runtime_exceptions flag is set. Otherwise, assertions are emitted.

Parameters

symbol_table	global symbol table, all of whose code members will be annotated (may gain exception type stubs and similar)
throw_runtime_exceptions	flag determining whether we instrument the code with runtime exceptions or with assertions. The former applies if this flag is set to true.
message_handler	stream to report status and warnings

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.

Exceptions are thrown when the throw_runtime_exceptions flag is set. Otherwise, assertions are emitted.

Parameters

symbol_table	global symbol table (may gain exception type stubs and similar)
symbol	the symbol to instrument
throw_runtime_exceptions	flag determining whether we instrument the code with runtime exceptions or with assertions. The former applies if this flag is set to true.
message_handler	stream to report status and warnings

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 entry point.

Parameters

init_code	the code block to which the assertion is appended
exc_symbol	the top-level exception symbol
source_location	the source location to attach to the assertion

const std::vector<std::string> exception_needed_classes

extern