Collaboration diagram for java_bytecode_instrumentt:

Public Member Functions
	java_bytecode_instrumentt (symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)

void	operator() (codet &code)
	Instruments `code`.

Protected Member Functions
code_ifthenelset	throw_exception (const exprt &cond, const source_locationt &original_loc, const irep_idt &exc_name)
	Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when cond is met.

codet	check_array_access (const exprt &array_struct, const exprt &idx, const source_locationt &original_loc)
	Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsException/generates an assertion if necessary; Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

codet	check_arithmetic_exception (const exprt &denominator, const source_locationt &original_loc)
	Checks whether there is a division by zero and throws ArithmeticException if necessary.

codet	check_null_dereference (const exprt &expr, const source_locationt &original_loc)
	Checks whether `expr` is null and throws NullPointerException/ generates an assertion when necessary; Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

code_ifthenelset	check_class_cast (const exprt &tested_expr, const struct_tag_typet &target_type, const source_locationt &original_loc)
	Checks whether `class1` is an instance of `class2` and throws ClassCastException/generates an assertion when necessary; Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

codet	check_array_length (const exprt &length, const source_locationt &original_loc)
	Checks whether `length` >= 0 and throws NegativeArraySizeException/ generates an assertion when necessary; Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

void	instrument_code (codet &code)
	Augments `code` with instrumentation in the form of either assertions or runtime exceptions.

void	add_expr_instrumentation (code_blockt &block, const exprt &expr)
	Checks whether `expr` requires instrumentation, and if so adds it to `block`.

void	prepend_instrumentation (codet &code, code_blockt &instrumentation)
	Appends `code` to `instrumentation` and overwrites reference `code` with the augmented block if `instrumentation` is non-empty.

std::optional< codet >	instrument_expr (const exprt &expr)
	Computes the instrumentation for `expr` in the form of either assertions or runtime exceptions.

Protected Attributes
symbol_table_baset &	symbol_table

const bool	throw_runtime_exceptions

message_handlert &	message_handler

Detailed Description

Definition at line 24 of file java_bytecode_instrument.cpp.

Constructor & Destructor Documentation

◆ java_bytecode_instrumentt()

java_bytecode_instrumentt::java_bytecode_instrumentt	(	symbol_table_baset &	_symbol_table,
		const bool	_throw_runtime_exceptions,
		message_handlert &	_message_handler
	)

inline

Definition at line 27 of file java_bytecode_instrument.cpp.

Member Function Documentation

◆ add_expr_instrumentation()

void java_bytecode_instrumentt::add_expr_instrumentation	(	code_blockt &	block,
		const exprt &	expr
	)

protected

Checks whether expr requires instrumentation, and if so adds it to block.

Parameters

[out]	block	block where instrumentation will be added
	expr	expression to instrument

Definition at line 308 of file java_bytecode_instrument.cpp.

◆ check_arithmetic_exception()

codet java_bytecode_instrumentt::check_arithmetic_exception	(	const exprt &	denominator,
		const source_locationt &	original_loc
	)

protected

Checks whether there is a division by zero and throws ArithmeticException if necessary.

Exceptions are thrown when the throw_runtime_exceptions flag is set.

Returns: Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ArithmeticException or asserts a nonzero denominator.

Definition at line 137 of file java_bytecode_instrument.cpp.

◆ check_array_access()

codet java_bytecode_instrumentt::check_array_access	(	const exprt &	array_struct,
		const exprt &	idx,
		const source_locationt &	original_loc
	)

protected

Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsException/generates an assertion if necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters

array_struct	array being accessed
idx	index into the array
original_loc	source location in the original code

Returns: Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ArrayIndexOutPfBoundsException or emits an assertion checking the array access

Definition at line 168 of file java_bytecode_instrument.cpp.

◆ check_array_length()

codet java_bytecode_instrumentt::check_array_length	(	const exprt &	length,
		const source_locationt &	original_loc
	)

protected

Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters

length	the checked length
original_loc	source location in the original code

Returns: Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an NegativeArraySizeException or emits an assertion checking the subtype relation

Definition at line 284 of file java_bytecode_instrument.cpp.

◆ check_class_cast()

code_ifthenelset java_bytecode_instrumentt::check_class_cast	(	const exprt &	tested_expr,
		const struct_tag_typet &	target_type,
		const source_locationt &	original_loc
	)

protected

Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters

tested_expr	expression to test
target_type	type to test for
original_loc	source location in the original code

Returns: Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an ClassCastException or emits an assertion checking the subtype relation

Definition at line 211 of file java_bytecode_instrument.cpp.

◆ check_null_dereference()

codet java_bytecode_instrumentt::check_null_dereference	(	const exprt &	expr,
		const source_locationt &	original_loc
	)

protected

Checks whether expr is null and throws NullPointerException/ generates an assertion when necessary; Exceptions are thrown when the throw_runtime_exceptions flag is set.

Otherwise, assertions are emitted.

Parameters

expr	the checked expression
original_loc	source location in the original code

Returns: Based on the value of the flag throw_runtime_exceptions, it returns code that either throws an NullPointerException or emits an assertion checking the subtype relation

Definition at line 255 of file java_bytecode_instrument.cpp.

◆ instrument_code()

void java_bytecode_instrumentt::instrument_code ( codet & code )

protected

Augments code with instrumentation in the form of either assertions or runtime exceptions.

Parameters

code	the expression to be instrumented

Definition at line 342 of file java_bytecode_instrument.cpp.

◆ instrument_expr()

std::optional< codet > java_bytecode_instrumentt::instrument_expr ( const exprt & expr )

protected

Computes the instrumentation for expr in the form of either assertions or runtime exceptions.

Parameters

expr	the expression for which we compute instrumentation

Returns: The instrumentation for expr if required

Definition at line 451 of file java_bytecode_instrument.cpp.

◆ operator()()

void java_bytecode_instrumentt::operator() ( codet & code )

Instruments code.

Parameters

code	the expression to be instrumented

Definition at line 528 of file java_bytecode_instrument.cpp.

◆ prepend_instrumentation()

void java_bytecode_instrumentt::prepend_instrumentation	(	codet &	code,
		code_blockt &	instrumentation
	)

protected

Appends code to instrumentation and overwrites reference code with the augmented block if instrumentation is non-empty.

Parameters

[in,out]	code	code being instrumented
	instrumentation	instrumentation code block to prepend

Definition at line 325 of file java_bytecode_instrument.cpp.

◆ throw_exception()

code_ifthenelset java_bytecode_instrumentt::throw_exception	(	const exprt &	cond,
		const source_locationt &	original_loc,
		const irep_idt &	exc_name
	)

protected

Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when cond is met.

Parameters

cond	condition to be met in order to throw an exception
original_loc	source location in the original program
exc_name	the name of the exception to be thrown

Returns: Returns the code initialising the throwing the exception

Definition at line 93 of file java_bytecode_instrument.cpp.

Member Data Documentation

◆ message_handler

message_handlert& java_bytecode_instrumentt::message_handler

protected

Definition at line 42 of file java_bytecode_instrument.cpp.

◆ symbol_table

symbol_table_baset& java_bytecode_instrumentt::symbol_table

protected

Definition at line 40 of file java_bytecode_instrument.cpp.

◆ throw_runtime_exceptions

const bool java_bytecode_instrumentt::throw_runtime_exceptions

protected

Definition at line 41 of file java_bytecode_instrument.cpp.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ java_bytecode_instrumentt()

Member Function Documentation

◆ add_expr_instrumentation()

◆ check_arithmetic_exception()

◆ check_array_access()

◆ check_array_length()

◆ check_class_cast()

◆ check_null_dereference()

◆ instrument_code()

◆ instrument_expr()

◆ operator()()

◆ prepend_instrumentation()

◆ throw_exception()

Member Data Documentation

◆ message_handler

◆ symbol_table

◆ throw_runtime_exceptions