CBMC
java_bytecode_parsert Member List
This is the complete list of members for
java_bytecode_parsert
, including all inherited members.
advance_column
(unsigned token_width)
parsert
inline
annotationt
typedef
java_bytecode_parsert
private
blue
messaget
static
bold
messaget
static
bright_blue
messaget
static
bright_cyan
messaget
static
bright_green
messaget
static
bright_magenta
messaget
static
bright_red
messaget
static
bright_yellow
messaget
static
classt
typedef
java_bytecode_parsert
private
clear
()
parsert
inline
virtual
column
parsert
protected
command
(unsigned c)
messaget
inline
static
conditional_output
(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
messaget
constant
(u2 index)
java_bytecode_parsert
inline
private
constant_pool
java_bytecode_parsert
private
constant_poolt
typedef
java_bytecode_parsert
private
cyan
messaget
static
debug
() const
messaget
inline
eof
()
parsert
inline
eom
messaget
static
error
() const
messaget
inline
eval_verbosity
(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
messaget
static
faint
messaget
static
fieldt
typedef
java_bytecode_parsert
private
get_annotation_class_refs
(const std::vector< annotationt > &annotations)
java_bytecode_parsert
private
get_annotation_value_class_refs
(const exprt &value)
java_bytecode_parsert
private
get_class_refs
()
java_bytecode_parsert
private
get_class_refs_rec
(const typet &)
java_bytecode_parsert
private
get_column
() const
parsert
inline
get_file
() const
parsert
inline
get_line_no
() const
parsert
inline
get_message_handler
()
messaget
inline
get_mstream
(unsigned message_level) const
messaget
inline
get_relement_value
()
java_bytecode_parsert
private
green
messaget
static
in
parsert
inc_line_no
()
parsert
inline
instructiont
typedef
java_bytecode_parsert
private
italic
messaget
static
java_bytecode_parsert
(bool skip_instructions)
java_bytecode_parsert
inline
explicit
lambda_method_handlet
typedef
java_bytecode_parsert
private
last_line
parsert
line_no
parsert
protected
M_DEBUG
enum value
messaget
M_ERROR
enum value
messaget
M_PROGRESS
enum value
messaget
M_RESULT
enum value
messaget
M_STATISTICS
enum value
messaget
M_STATUS
enum value
messaget
M_WARNING
enum value
messaget
magenta
messaget
static
message_handler
messaget
protected
message_levelt
enum name
messaget
messaget
()
messaget
inline
messaget
(const messaget &other)
messaget
inline
messaget
(message_handlert &_message_handler)
messaget
inline
explicit
method_handle_typet
typedef
java_bytecode_parsert
private
methodt
typedef
java_bytecode_parsert
private
mstream
messaget
mutable
protected
operator=
(const messaget &other)
messaget
inline
parse
() override
java_bytecode_parsert
virtual
parse_error
(const std::string &message, const std::string &before)
parsert
parse_local_variable_type_table
(methodt &method)
java_bytecode_parsert
private
parse_method_handle
(const class method_handle_infot &entry)
java_bytecode_parsert
private
parse_tree
java_bytecode_parsert
parsert
()
parsert
inline
pool_entry
(u2 index)
java_bytecode_parsert
inline
private
previous_line_no
parsert
protected
progress
() const
messaget
inline
rbytecode
(std::vector< instructiont > &)
java_bytecode_parsert
private
rclass_attribute
()
java_bytecode_parsert
private
rClassFile
()
java_bytecode_parsert
private
rcode_attribute
(methodt &method)
java_bytecode_parsert
private
rconstant_pool
()
java_bytecode_parsert
private
read
()
java_bytecode_parsert
inline
private
parsert::read
(char &ch)
parsert
inline
read_bootstrapmethods_entry
()
java_bytecode_parsert
private
read_verification_type_info
(methodt::verification_type_infot &)
java_bytecode_parsert
private
red
messaget
static
relement_value_pairs
(annotationt::element_value_pairst &)
java_bytecode_parsert
private
reset
messaget
static
result
() const
messaget
inline
rexceptions_attribute
()
java_bytecode_parsert
private
rfield_attribute
(fieldt &)
java_bytecode_parsert
private
rfields
()
java_bytecode_parsert
private
rinner_classes_attribute
(const u4 &attribute_length)
java_bytecode_parsert
private
rinterfaces
()
java_bytecode_parsert
private
rmethod
()
java_bytecode_parsert
private
rmethod_attribute
(methodt &method)
java_bytecode_parsert
private
rmethods
()
java_bytecode_parsert
private
rRuntimeAnnotation
(annotationt &)
java_bytecode_parsert
private
rRuntimeAnnotation_attribute
(std::vector< annotationt > &)
java_bytecode_parsert
private
set_column
(unsigned _column)
parsert
inline
set_file
(const irep_idt &file)
parsert
inline
set_function
(const irep_idt &function)
parsert
inline
set_line_no
(unsigned _line_no)
parsert
inline
set_message_handler
(message_handlert &_message_handler)
messaget
inline
virtual
set_source_location
(exprt &e)
parsert
inline
skip_bytes
(std::size_t bytes)
java_bytecode_parsert
inline
private
skip_instructions
java_bytecode_parsert
private
source_location
parsert
protected
stack
parsert
statistics
() const
messaget
inline
status
() const
messaget
inline
store_unknown_method_handle
(size_t bootstrap_method_index)
java_bytecode_parsert
private
this_line
parsert
type_entry
(u2 index)
java_bytecode_parsert
inline
private
underline
messaget
static
warning
() const
messaget
inline
yellow
messaget
static
~messaget
()
messaget
virtual
~parsert
()
parsert
inline
virtual
Generated by
1.8.17