CBMC
java_bytecode_instrument.cpp File Reference
+ Include dependency graph for java_bytecode_instrument.cpp:

Go to the source code of this file.

Classes

class  java_bytecode_instrumentt
 

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

Variables

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

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_tableglobal symbol table, all of whose code members will be annotated (may gain exception type stubs and similar)
throw_runtime_exceptionsflag determining whether we instrument the code with runtime exceptions or with assertions. The former applies if this flag is set to true.
message_handlerstream to report status and warnings

Definition at line 594 of file java_bytecode_instrument.cpp.

◆ java_bytecode_instrument_symbol()

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_tableglobal symbol table (may gain exception type stubs and similar)
symbolthe symbol to instrument
throw_runtime_exceptionsflag determining whether we instrument the code with runtime exceptions or with assertions. The former applies if this flag is set to true.
message_handlerstream to report status and warnings

Definition at line 544 of file java_bytecode_instrument.cpp.

◆ java_bytecode_instrument_uncaught_exceptions()

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_codethe code block to which the assertion is appended
exc_symbolthe top-level exception symbol
source_locationthe source location to attach to the assertion

Definition at line 567 of file java_bytecode_instrument.cpp.

Variable Documentation

◆ exception_needed_classes

const std::vector<std::string> exception_needed_classes
Initial value:
= {
"java.lang.ArithmeticException",
"java.lang.ArrayIndexOutOfBoundsException",
"java.lang.ClassCastException",
"java.lang.NegativeArraySizeException",
"java.lang.NullPointerException"}

Definition at line 77 of file java_bytecode_instrument.cpp.