CBMC
Loading...
Searching...
No Matches
Functions | Variables
java_bytecode_instrument.h File Reference
#include <string>
#include <vector>
+ Include dependency graph for java_bytecode_instrument.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

  Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
 
  Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions.
 
  Instruments the start function with an assertion that checks whether an exception has escaped the entry point.
 

Variables

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

Function Documentation

◆  java_bytecode_instrument()

void java_bytecode_instrument ( symbol_table_basetsymbol_table,
const bool  throw_runtime_exceptions,
message_handlertmessage_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

Definition at line 594 of file java_bytecode_instrument.cpp.

◆  java_bytecode_instrument_symbol()

void java_bytecode_instrument_symbol ( symbol_table_basetsymbol_table,
symboltsymbol,
const bool  throw_runtime_exceptions,
message_handlertmessage_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

Definition at line 544 of file java_bytecode_instrument.cpp.

◆  java_bytecode_instrument_uncaught_exceptions()

void java_bytecode_instrument_uncaught_exceptions ( code_blocktinit_code,
const symboltexc_symbol,
const source_locationtsource_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

Definition at line 567 of file java_bytecode_instrument.cpp.

Variable Documentation

◆  exception_needed_classes

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

Definition at line 77 of file java_bytecode_instrument.cpp.

AltStyle によって変換されたページ (->オリジナル) /