cprover
java_bytecode_instrumentt Member List

This is the complete list of members for java_bytecode_instrumentt, including all inherited members.

add_expr_instrumentation(code_blockt &block, const exprt &expr)java_bytecode_instrumenttprotected
bluemessagetstatic
boldmessagetstatic
bright_bluemessagetstatic
bright_cyanmessagetstatic
bright_greenmessagetstatic
bright_magentamessagetstatic
bright_redmessagetstatic
bright_yellowmessagetstatic
check_arithmetic_exception(const exprt &denominator, const source_locationt &original_loc)java_bytecode_instrumenttprotected
check_array_access(const exprt &array_struct, const exprt &idx, const source_locationt &original_loc)java_bytecode_instrumenttprotected
check_array_length(const exprt &length, const source_locationt &original_loc)java_bytecode_instrumenttprotected
check_class_cast(const exprt &tested_expr, const struct_tag_typet &target_type, const source_locationt &original_loc)java_bytecode_instrumenttprotected
check_null_dereference(const exprt &expr, const source_locationt &original_loc)java_bytecode_instrumenttprotected
command(unsigned c)messagetinlinestatic
conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) constmessaget
cyanmessagetstatic
debug() constmessagetinline
eommessagetstatic
error() constmessagetinline
eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)messagetstatic
faintmessagetstatic
get_message_handler()messagetinline
get_mstream(unsigned message_level) constmessagetinline
greenmessagetstatic
instrument_code(codet &code)java_bytecode_instrumenttprotected
instrument_expr(const exprt &expr)java_bytecode_instrumenttprotected
italicmessagetstatic
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)java_bytecode_instrumenttinline
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
magentamessagetstatic
message_handlerjava_bytecode_instrumenttprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetmutableprotected
operator()(codet &code)java_bytecode_instrumentt
operator=(const messaget &other)messagetinline
prepend_instrumentation(codet &code, code_blockt &instrumentation)java_bytecode_instrumenttprotected
progress() constmessagetinline
redmessagetstatic
resetmessagetstatic
result() constmessagetinline
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
statistics() constmessagetinline
status() constmessagetinline
symbol_tablejava_bytecode_instrumenttprotected
throw_exception(const exprt &cond, const source_locationt &original_loc, const irep_idt &exc_name)java_bytecode_instrumenttprotected
throw_runtime_exceptionsjava_bytecode_instrumenttprotected
underlinemessagetstatic
warning() constmessagetinline
yellowmessagetstatic
~messaget()messagetvirtual