cprover
|
Classes | |
class | bytecodet |
struct | pool_entryt |
Public Types | |
typedef java_bytecode_parse_treet::classt | classt |
typedef java_bytecode_parse_treet::classt::fieldst | fieldst |
typedef java_bytecode_parse_treet::classt::methodst | methodst |
typedef java_bytecode_parse_treet::methodt | methodt |
typedef java_bytecode_parse_treet::fieldt | fieldt |
typedef java_bytecode_parse_treet::methodt::instructionst | instructionst |
typedef java_bytecode_parse_treet::instructiont | instructiont |
typedef java_bytecode_parse_treet::annotationt | annotationt |
typedef java_bytecode_parse_treet::annotationst | annotationst |
typedef std::vector< pool_entryt > | constant_poolt |
Public Member Functions | |
java_bytecode_parsert () | |
virtual bool | parse () |
![]() | |
virtual void | clear () |
parsert () | |
virtual | ~parsert () |
bool | read (char &ch) |
bool | eof () |
void | parse_error (const std::string &message, const std::string &before) |
void | inc_line_no () |
void | set_line_no (unsigned _line_no) |
void | set_file (const irep_idt &file) |
irep_idt | get_file () const |
unsigned | get_line_no () const |
unsigned | get_column () const |
void | set_column (unsigned _column) |
void | set_source_location (exprt &e) |
void | set_function (const irep_idt &function) |
void | advance_column (unsigned token_width) |
Public Attributes | |
java_bytecode_parse_treet | parse_tree |
constant_poolt | constant_pool |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Protected Attributes | |
std::vector< bytecodet > | bytecodes |
![]() | |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Additional Inherited Members |
Definition at line 32 of file java_bytecode_parser.cpp.
Definition at line 50 of file java_bytecode_parser.cpp.
Definition at line 49 of file java_bytecode_parser.cpp.
Definition at line 42 of file java_bytecode_parser.cpp.
typedef std::vector<pool_entryt> java_bytecode_parsert::constant_poolt |
Definition at line 64 of file java_bytecode_parser.cpp.
Definition at line 43 of file java_bytecode_parser.cpp.
Definition at line 46 of file java_bytecode_parser.cpp.
Definition at line 47 of file java_bytecode_parser.cpp.
Definition at line 48 of file java_bytecode_parser.cpp.
Definition at line 44 of file java_bytecode_parser.cpp.
Definition at line 45 of file java_bytecode_parser.cpp.
|
inline |
Definition at line 35 of file java_bytecode_parser.cpp.
References get_bytecodes(), and parse().
Definition at line 88 of file java_bytecode_parser.cpp.
References java_bytecode_parsert::pool_entryt::expr, and pool_entry().
Referenced by rbytecode(), rClassFile(), relement_value_pair(), and rinterfaces().
|
inlineprotected |
Definition at line 98 of file java_bytecode_parser.cpp.
References bytecode_info, get_class_refs(), get_class_refs_rec(), bytecode_infot::mnemonic, rbytecode(), rclass_attribute(), rClassFile(), rcode_attribute(), rconstant_pool(), read_verification_type_info(), relement_value_pair(), relement_value_pairs(), rfield_attribute(), rfields(), rinterfaces(), rmethod(), rmethod_attribute(), rmethods(), rRuntimeAnnotation(), and rRuntimeAnnotation_attribute().
Referenced by java_bytecode_parsert().
|
protected |
Definition at line 309 of file java_bytecode_parser.cpp.
References CONSTANT_Class, CONSTANT_NameAndType, constant_pool, java_bytecode_parse_treet::classt::fields, get_class_refs_rec(), id2string(), java_type_from_string(), java_bytecode_parse_treet::classt::methods, parse_tree, java_bytecode_parse_treet::parsed_class, pool_entry(), and java_bytecode_parsert::pool_entryt::s.
Referenced by get_bytecodes(), and rClassFile().
|
protected |
Definition at line 351 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::class_refs, struct_union_typet::components(), irept::find(), irept::get(), has_prefix(), irept::id(), id2string(), code_typet::parameters(), parse_tree, code_typet::return_type(), typet::subtype(), to_code_type(), and to_struct_type().
Referenced by get_bytecodes(), and get_class_refs().
|
virtual |
Implements parsert.
Definition at line 204 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), and rClassFile().
Referenced by java_bytecode_parse(), and java_bytecode_parsert().
|
inlineprotected |
Definition at line 77 of file java_bytecode_parser.cpp.
References messaget::eom(), and messaget::error().
Referenced by constant(), get_class_refs(), rclass_attribute(), rcode_attribute(), rconstant_pool(), relement_value_pair(), relement_value_pairs(), rfield_attribute(), rfields(), rmethod(), rmethod_attribute(), and type_entry().
|
protected |
Definition at line 651 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::instructiont::address, java_bytecode_parse_treet::instructiont::args, bytecodes, constant(), messaget::eom(), messaget::error(), from_integer(), irept::id(), read_u1(), read_u2(), read_u4(), java_bytecode_parsert::pool_entryt::s, source_locationt::set_java_bytecode_index(), java_bytecode_parse_treet::instructiont::source_location, java_bytecode_parse_treet::instructiont::statement, T_BOOLEAN, T_BYTE, T_CHAR, T_DOUBLE, T_FLOAT, T_INT, T_LONG, and T_SHORT.
Referenced by get_bytecodes(), and rmethod_attribute().
|
protected |
Definition at line 1268 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::classt::annotations, id2string(), java_bytecode_parse_treet::classt::methods, java_bytecode_parse_treet::classt::name, pool_entry(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, and skip_bytes().
Referenced by get_bytecodes(), and rClassFile().
|
protected |
Definition at line 252 of file java_bytecode_parser.cpp.
References ACC_ABSTRACT, ACC_ENUM, constant(), java_bytecode_parse_treet::classt::enum_elements, messaget::eom(), messaget::error(), java_bytecode_parse_treet::classt::extends, java_bytecode_parse_treet::classt::fields, irept::get(), get_class_refs(), java_bytecode_parse_treet::classt::is_abstract, java_bytecode_parse_treet::fieldt::is_enum, java_bytecode_parse_treet::classt::is_enum, java_bytecode_parse_treet::loading_successful, java_bytecode_parse_treet::classt::name, parse_tree, java_bytecode_parse_treet::parsed_class, rclass_attribute(), rconstant_pool(), read_u2(), read_u4(), rfields(), rinterfaces(), rmethods(), exprt::type(), and UNUSED.
Referenced by get_bytecodes(), and parse().
|
protected |
Definition at line 969 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::methodt::stack_map_table_entryt::APPEND, java_bytecode_parse_treet::methodt::stack_map_table_entryt::CHOP, java_bytecode_parse_treet::methodt::stack_map_table_entryt::FULL, id2string(), java_bytecode_parse_treet::methodt::instructions, java_bytecode_parse_treet::methodt::local_variable_table, pool_entry(), read_u1(), read_u2(), read_u4(), read_verification_type_info(), java_bytecode_parsert::pool_entryt::s, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_EXTENDED, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK, java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK_EXTENDED, skip_bytes(), and java_bytecode_parse_treet::methodt::stack_map_table.
Referenced by get_bytecodes(), and rmethod_attribute().
|
protected |
Definition at line 383 of file java_bytecode_parser.cpp.
References CONSTANT_Class, CONSTANT_Double, CONSTANT_Fieldref, CONSTANT_Float, CONSTANT_Integer, CONSTANT_InterfaceMethodref, CONSTANT_InvokeDynamic, CONSTANT_Long, CONSTANT_MethodHandle, CONSTANT_Methodref, CONSTANT_MethodType, CONSTANT_NameAndType, constant_pool, CONSTANT_String, CONSTANT_Utf8, ieee_float_spect::double_precision(), messaget::eom(), messaget::error(), from_integer(), symbol_typet::get_identifier(), id2string(), java_classname(), java_int_type(), java_long_type(), pool_entry(), read_u1(), read_u2(), read_u4(), read_u8(), java_bytecode_parsert::pool_entryt::ref1, java_bytecode_parsert::pool_entryt::ref2, java_bytecode_parsert::pool_entryt::s, irept::set(), ieee_float_spect::single_precision(), ieee_floatt::to_expr(), type_entry(), and ieee_floatt::unpack().
Referenced by get_bytecodes(), and rClassFile().
|
inlineprotected |
Definition at line 142 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), parsert::in, and messaget::result().
Referenced by read_u1(), read_u2(), read_u4(), and read_u8().
|
inlineprotected |
Definition at line 158 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rbytecode(), rcode_attribute(), rconstant_pool(), read_verification_type_info(), and relement_value_pair().
|
inlineprotected |
Definition at line 163 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rbytecode(), rclass_attribute(), rClassFile(), rcode_attribute(), rconstant_pool(), read_verification_type_info(), relement_value_pair(), relement_value_pairs(), rfield_attribute(), rfields(), rinterfaces(), rmethod(), rmethod_attribute(), rmethods(), rRuntimeAnnotation(), and rRuntimeAnnotation_attribute().
|
inlineprotected |
Definition at line 168 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rbytecode(), rclass_attribute(), rClassFile(), rcode_attribute(), rconstant_pool(), rfield_attribute(), and rmethod_attribute().
|
inlineprotected |
Definition at line 173 of file java_bytecode_parser.cpp.
References read_bytes().
Referenced by rconstant_pool().
|
protected |
Definition at line 1133 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index, java_bytecode_parse_treet::methodt::verification_type_infot::DOUBLE, java_bytecode_parse_treet::methodt::verification_type_infot::FLOAT, java_bytecode_parse_treet::methodt::verification_type_infot::INTEGER, java_bytecode_parse_treet::methodt::verification_type_infot::ITEM_NULL, java_bytecode_parse_treet::methodt::verification_type_infot::LONG, java_bytecode_parse_treet::methodt::verification_type_infot::OBJECT, java_bytecode_parse_treet::methodt::verification_type_infot::offset, read_u1(), read_u2(), java_bytecode_parsert::pool_entryt::tag, java_bytecode_parse_treet::methodt::verification_type_infot::TOP, java_bytecode_parse_treet::methodt::verification_type_infot::type, java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED, java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED_THIS, VTYPE_INFO_DOUBLE, VTYPE_INFO_FLOAT, VTYPE_INFO_INTEGER, VTYPE_INFO_ITEM_NULL, VTYPE_INFO_LONG, VTYPE_INFO_OBJECT, VTYPE_INFO_TOP, VTYPE_INFO_UNINIT, and VTYPE_INFO_UNINIT_THIS.
Referenced by get_bytecodes(), and rcode_attribute().
|
protected |
Definition at line 1209 of file java_bytecode_parser.cpp.
References constant(), pool_entry(), read_u1(), read_u2(), rRuntimeAnnotation(), java_bytecode_parsert::pool_entryt::s, java_bytecode_parsert::pool_entryt::tag, UNUSED, and java_bytecode_parse_treet::annotationt::element_value_pairt::value.
Referenced by get_bytecodes(), and relement_value_pairs().
|
protected |
Definition at line 1194 of file java_bytecode_parser.cpp.
References pool_entry(), read_u2(), relement_value_pair(), and java_bytecode_parsert::pool_entryt::s.
Referenced by get_bytecodes(), and rRuntimeAnnotation().
|
protected |
Definition at line 953 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::membert::annotations, pool_entry(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, and skip_bytes().
Referenced by get_bytecodes(), and rfields().
|
protected |
Definition at line 611 of file java_bytecode_parser.cpp.
References ACC_ENUM, ACC_FINAL, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, java_bytecode_parse_treet::classt::add_field(), id2string(), java_bytecode_parse_treet::fieldt::is_enum, java_bytecode_parse_treet::membert::is_final, java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_bytecode_parse_treet::membert::name, pool_entry(), read_u2(), rfield_attribute(), java_bytecode_parsert::pool_entryt::s, and java_bytecode_parse_treet::membert::signature.
Referenced by get_bytecodes(), and rClassFile().
|
protected |
Definition at line 602 of file java_bytecode_parser.cpp.
References constant(), java_bytecode_parse_treet::classt::implements, and read_u2().
Referenced by get_bytecodes(), and rClassFile().
|
protected |
Definition at line 1338 of file java_bytecode_parser.cpp.
References ACC_ABSTRACT, ACC_FINAL, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_SYNCHRONIZED, java_bytecode_parse_treet::classt::add_method(), java_bytecode_parse_treet::methodt::base_name, id2string(), java_bytecode_parse_treet::methodt::is_abstract, java_bytecode_parse_treet::membert::is_final, java_bytecode_parse_treet::methodt::is_native, java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_bytecode_parse_treet::methodt::is_synchronized, java_bytecode_parse_treet::membert::name, pool_entry(), read_u2(), rmethod_attribute(), java_bytecode_parsert::pool_entryt::s, and java_bytecode_parse_treet::membert::signature.
Referenced by get_bytecodes(), and rmethods().
|
protected |
Definition at line 885 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::membert::annotations, dstringt::empty(), java_bytecode_parse_treet::methodt::exception_table, java_bytecode_parsert::pool_entryt::expr, id2string(), java_bytecode_parse_treet::methodt::instructions, java_bytecode_parse_treet::membert::name, java_bytecode_parse_treet::classt::name, parse_tree, java_bytecode_parse_treet::parsed_class, pool_entry(), rbytecode(), rcode_attribute(), read_u2(), read_u4(), rRuntimeAnnotation_attribute(), java_bytecode_parsert::pool_entryt::s, source_locationt::set_line(), java_bytecode_parse_treet::membert::signature, skip_bytes(), java_bytecode_parse_treet::methodt::source_location, to_symbol_type(), exprt::type(), and UNUSED.
Referenced by get_bytecodes(), and rmethod().
|
protected |
Definition at line 1316 of file java_bytecode_parser.cpp.
References read_u2(), and rmethod().
Referenced by get_bytecodes(), and rClassFile().
|
protected |
Definition at line 1186 of file java_bytecode_parser.cpp.
References java_bytecode_parse_treet::annotationt::element_value_pairs, read_u2(), relement_value_pairs(), java_bytecode_parse_treet::annotationt::type, and type_entry().
Referenced by get_bytecodes(), relement_value_pair(), and rRuntimeAnnotation_attribute().
|
protected |
Definition at line 1173 of file java_bytecode_parser.cpp.
References java_bytecode_parsert::pool_entryt::number, read_u2(), and rRuntimeAnnotation().
Referenced by get_bytecodes(), rclass_attribute(), rfield_attribute(), and rmethod_attribute().
|
inlineprotected |
Definition at line 129 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), and parsert::in.
Referenced by rclass_attribute(), rcode_attribute(), rfield_attribute(), and rmethod_attribute().
Definition at line 93 of file java_bytecode_parser.cpp.
References id2string(), java_type_from_string(), pool_entry(), and java_bytecode_parsert::pool_entryt::s.
Referenced by rconstant_pool(), and rRuntimeAnnotation().
|
protected |
Definition at line 75 of file java_bytecode_parser.cpp.
Referenced by rbytecode().
constant_poolt java_bytecode_parsert::constant_pool |
Definition at line 65 of file java_bytecode_parser.cpp.
Referenced by get_class_refs(), and rconstant_pool().
java_bytecode_parse_treet java_bytecode_parsert::parse_tree |
Definition at line 52 of file java_bytecode_parser.cpp.
Referenced by get_class_refs(), get_class_refs_rec(), java_bytecode_parse(), rClassFile(), and rmethod_attribute().