cprover
|
#include "java_bytecode_parser.h"
#include <algorithm>
#include <fstream>
#include <map>
#include <string>
#include <util/parser.h>
#include <util/std_expr.h>
#include <util/arith_tools.h>
#include <util/ieee_float.h>
#include <util/prefix.h>
#include <ansi-c/string_constant.h>
#include "java_bytecode_parse_tree.h"
#include "java_types.h"
#include "bytecode_info.h"
Go to the source code of this file.
Classes | |
class | java_bytecode_parsert |
struct | java_bytecode_parsert::pool_entryt |
class | java_bytecode_parsert::bytecodet |
Macros | |
#define | CONSTANT_Class 7 |
#define | CONSTANT_Fieldref 9 |
#define | CONSTANT_Methodref 10 |
#define | CONSTANT_InterfaceMethodref 11 |
#define | CONSTANT_String 8 |
#define | CONSTANT_Integer 3 |
#define | CONSTANT_Float 4 |
#define | CONSTANT_Long 5 |
#define | CONSTANT_Double 6 |
#define | CONSTANT_NameAndType 12 |
#define | CONSTANT_Utf8 1 |
#define | CONSTANT_MethodHandle 15 |
#define | CONSTANT_MethodType 16 |
#define | CONSTANT_InvokeDynamic 18 |
#define | VTYPE_INFO_TOP 0 |
#define | VTYPE_INFO_INTEGER 1 |
#define | VTYPE_INFO_FLOAT 2 |
#define | VTYPE_INFO_LONG 3 |
#define | VTYPE_INFO_DOUBLE 4 |
#define | VTYPE_INFO_ITEM_NULL 5 |
#define | VTYPE_INFO_UNINIT_THIS 6 |
#define | VTYPE_INFO_OBJECT 7 |
#define | VTYPE_INFO_UNINIT 8 |
#define | ACC_PUBLIC 0x0001 |
#define | ACC_PRIVATE 0x0002 |
#define | ACC_PROTECTED 0x0004 |
#define | ACC_STATIC 0x0008 |
#define | ACC_FINAL 0x0010 |
#define | ACC_SYNCHRONIZED 0x0020 |
#define | ACC_BRIDGE 0x0040 |
#define | ACC_VARARGS 0x0080 |
#define | ACC_NATIVE 0x0100 |
#define | ACC_ABSTRACT 0x0400 |
#define | ACC_STRICT 0x0800 |
#define | ACC_SYNTHETIC 0x1000 |
#define | ACC_ENUM 0x4000 |
#define | UNUSED __attribute__((unused)) |
#define | T_BOOLEAN 4 |
#define | T_CHAR 5 |
#define | T_FLOAT 6 |
#define | T_DOUBLE 7 |
#define | T_BYTE 8 |
#define | T_SHORT 9 |
#define | T_INT 10 |
#define | T_LONG 11 |
#define | ACC_PUBLIC 0x0001 |
#define | ACC_PRIVATE 0x0002 |
#define | ACC_PROTECTED 0x0004 |
#define | ACC_STATIC 0x0008 |
#define | ACC_FINAL 0x0010 |
#define | ACC_SUPER 0x0020 |
#define | ACC_VOLATILE 0x0040 |
#define | ACC_TRANSIENT 0x0080 |
#define | ACC_INTERFACE 0x0200 |
#define | ACC_ABSTRACT 0x0400 |
#define | ACC_SYNTHETIC 0x1000 |
#define | ACC_ANNOTATION 0x2000 |
#define | ACC_ENUM 0x4000 |
Functions | |
bool | java_bytecode_parse (std::istream &istream, java_bytecode_parse_treet &parse_tree, message_handlert &message_handler) |
bool | java_bytecode_parse (const std::string &file, java_bytecode_parse_treet &parse_tree, message_handlert &message_handler) |
#define ACC_ABSTRACT 0x0400 |
Definition at line 1333 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), and java_bytecode_parsert::rmethod().
#define ACC_ABSTRACT 0x0400 |
Definition at line 1333 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000 |
Definition at line 1335 of file java_bytecode_parser.cpp.
#define ACC_BRIDGE 0x0040 |
Definition at line 238 of file java_bytecode_parser.cpp.
#define ACC_ENUM 0x4000 |
Definition at line 1336 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), and java_bytecode_parsert::rfields().
#define ACC_ENUM 0x4000 |
Definition at line 1336 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010 |
Definition at line 1328 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_FINAL 0x0010 |
Definition at line 1328 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200 |
Definition at line 1332 of file java_bytecode_parser.cpp.
#define ACC_NATIVE 0x0100 |
Definition at line 240 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rmethod().
#define ACC_PRIVATE 0x0002 |
Definition at line 1325 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_PRIVATE 0x0002 |
Definition at line 1325 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004 |
Definition at line 1326 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_PROTECTED 0x0004 |
Definition at line 1326 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001 |
Definition at line 1324 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_PUBLIC 0x0001 |
Definition at line 1324 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008 |
Definition at line 1327 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rfields(), and java_bytecode_parsert::rmethod().
#define ACC_STATIC 0x0008 |
Definition at line 1327 of file java_bytecode_parser.cpp.
#define ACC_STRICT 0x0800 |
Definition at line 242 of file java_bytecode_parser.cpp.
#define ACC_SUPER 0x0020 |
Definition at line 1329 of file java_bytecode_parser.cpp.
#define ACC_SYNCHRONIZED 0x0020 |
Definition at line 237 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rmethod().
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1334 of file java_bytecode_parser.cpp.
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1334 of file java_bytecode_parser.cpp.
#define ACC_TRANSIENT 0x0080 |
Definition at line 1331 of file java_bytecode_parser.cpp.
#define ACC_VARARGS 0x0080 |
Definition at line 239 of file java_bytecode_parser.cpp.
#define ACC_VOLATILE 0x0040 |
Definition at line 1330 of file java_bytecode_parser.cpp.
#define CONSTANT_Class 7 |
Definition at line 179 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::get_class_refs(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Double 6 |
Definition at line 187 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Fieldref 9 |
Definition at line 180 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Float 4 |
Definition at line 185 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Integer 3 |
Definition at line 184 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_InterfaceMethodref 11 |
Definition at line 182 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_InvokeDynamic 18 |
Definition at line 192 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Long 5 |
Definition at line 186 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_MethodHandle 15 |
Definition at line 190 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Methodref 10 |
Definition at line 181 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_MethodType 16 |
Definition at line 191 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_NameAndType 12 |
Definition at line 188 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::get_class_refs(), and java_bytecode_parsert::rconstant_pool().
#define CONSTANT_String 8 |
Definition at line 183 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define CONSTANT_Utf8 1 |
Definition at line 189 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rconstant_pool().
#define T_BOOLEAN 4 |
Definition at line 642 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_BYTE 8 |
Definition at line 646 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_CHAR 5 |
Definition at line 643 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_DOUBLE 7 |
Definition at line 645 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_FLOAT 6 |
Definition at line 644 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_INT 10 |
Definition at line 648 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_LONG 11 |
Definition at line 649 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define T_SHORT 9 |
Definition at line 647 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rbytecode().
#define UNUSED __attribute__((unused)) |
Definition at line 249 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::rClassFile(), java_bytecode_parsert::relement_value_pair(), and java_bytecode_parsert::rmethod_attribute().
#define VTYPE_INFO_DOUBLE 4 |
Definition at line 198 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_FLOAT 2 |
Definition at line 196 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_INTEGER 1 |
Definition at line 195 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_ITEM_NULL 5 |
Definition at line 199 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_LONG 3 |
Definition at line 197 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_OBJECT 7 |
Definition at line 201 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_TOP 0 |
Definition at line 194 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_UNINIT 8 |
Definition at line 202 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
#define VTYPE_INFO_UNINIT_THIS 6 |
Definition at line 200 of file java_bytecode_parser.cpp.
Referenced by java_bytecode_parsert::read_verification_type_info().
bool java_bytecode_parse | ( | std::istream & | istream, |
java_bytecode_parse_treet & | parse_tree, | ||
message_handlert & | message_handler | ||
) |
Definition at line 1368 of file java_bytecode_parser.cpp.
References parsert::in, java_bytecode_parsert::parse(), java_bytecode_parsert::parse_tree, messaget::set_message_handler(), and java_bytecode_parse_treet::swap().
Referenced by java_class_loadert::get_parse_tree(), and java_bytecode_parse().
bool java_bytecode_parse | ( | const std::string & | file, |
java_bytecode_parse_treet & | parse_tree, | ||
message_handlert & | message_handler | ||
) |
Definition at line 1384 of file java_bytecode_parser.cpp.
References messaget::eom(), messaget::error(), parsert::in, and java_bytecode_parse().