Loading...

Searching...

No Matches

Public Member Functions | Protected Member Functions | Protected Attributes | List of all members

java_bytecode_instrumentt Class Reference

+ 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