cprover
java_bytecode_instrumentt Class Reference
+ Inheritance diagram for java_bytecode_instrumentt:
+ 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. More...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
void instrument_code (codet &code)
 Augments code with instrumentation in the form of either assertions or runtime exceptions. More...
 
void add_expr_instrumentation (code_blockt &block, const exprt &expr)
 Checks whether expr requires instrumentation, and if so adds it to block. More...
 
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. More...
 
optionalt< codetinstrument_expr (const exprt &expr)
 Computes the instrumentation for expr in the form of either assertions or runtime exceptions. More...
 

Protected Attributes

symbol_table_basetsymbol_table
 
const bool throw_runtime_exceptions
 
message_handlertmessage_handler
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 25 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 28 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]blockblock where instrumentation will be added
exprexpression to instrument

Definition at line 310 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 139 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_structarray being accessed
idxindex into the array
original_locsource 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 170 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
lengththe checked length
original_locsource 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 286 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_exprexpression to test
target_typetype to test for
original_locsource 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 213 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
exprthe checked expression
original_locsource 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 257 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
codethe expression to be instrumented

Definition at line 344 of file java_bytecode_instrument.cpp.

◆ instrument_expr()

optionalt< 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
exprthe expression for which we compute instrumentation
Returns
The instrumentation for expr if required

Definition at line 452 of file java_bytecode_instrument.cpp.

◆ operator()()

void java_bytecode_instrumentt::operator() ( codet code)

Instruments code.

Parameters
codethe expression to be instrumented

Definition at line 529 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]codecode being instrumented
instrumentationinstrumentation code block to prepend

Definition at line 327 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
condcondition to be met in order to throw an exception
original_locsource location in the original program
exc_namethe name of the exception to be thrown
Returns
Returns the code initialising the throwing the exception

Definition at line 95 of file java_bytecode_instrument.cpp.

Member Data Documentation

◆ message_handler

message_handlert& java_bytecode_instrumentt::message_handler
protected

Definition at line 44 of file java_bytecode_instrument.cpp.

◆ symbol_table

symbol_table_baset& java_bytecode_instrumentt::symbol_table
protected

Definition at line 42 of file java_bytecode_instrument.cpp.

◆ throw_runtime_exceptions

const bool java_bytecode_instrumentt::throw_runtime_exceptions
protected

Definition at line 43 of file java_bytecode_instrument.cpp.


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