cprover
|
#include "java_bytecode_parser.h"
#include <algorithm>
#include <fstream>
#include <map>
#include <string>
#include <util/arith_tools.h>
#include <util/ieee_float.h>
#include <util/parser.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/string_constant.h>
#include <util/optional.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 |
class | structured_pool_entryt |
class | class_infot |
Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1. More... | |
class | name_and_type_infot |
Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6. More... | |
class | base_ref_infot |
class | method_handle_infot |
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_NATIVE 0x0100 |
#define | ACC_INTERFACE 0x0200 |
#define | ACC_ABSTRACT 0x0400 |
#define | ACC_STRICT 0x0800 |
#define | ACC_SYNTHETIC 0x1000 |
#define | ACC_ANNOTATION 0x2000 |
#define | ACC_ENUM 0x4000 |
#define | UNUSED_u2(x) { const u2 x = read_u2(); (void)x; } (void)0 |
#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_VARARGS 0x0080 |
#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 | |
optionalt< java_bytecode_parse_treet > | java_bytecode_parse (std::istream &istream, message_handlert &message_handler, bool skip_instructions) |
Attempt to parse a Java class from the given stream. More... | |
optionalt< java_bytecode_parse_treet > | java_bytecode_parse (const std::string &file, message_handlert &message_handler, bool skip_instructions) |
Attempt to parse a Java class from the given file. More... | |
#define ACC_ABSTRACT 0x0400 |
Definition at line 1832 of file java_bytecode_parser.cpp.
#define ACC_ABSTRACT 0x0400 |
Definition at line 1832 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000 |
Definition at line 1834 of file java_bytecode_parser.cpp.
#define ACC_ANNOTATION 0x2000 |
Definition at line 1834 of file java_bytecode_parser.cpp.
#define ACC_BRIDGE 0x0040 |
Definition at line 464 of file java_bytecode_parser.cpp.
#define ACC_ENUM 0x4000 |
Definition at line 1835 of file java_bytecode_parser.cpp.
#define ACC_ENUM 0x4000 |
Definition at line 1835 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010 |
Definition at line 1826 of file java_bytecode_parser.cpp.
#define ACC_FINAL 0x0010 |
Definition at line 1826 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200 |
Definition at line 1831 of file java_bytecode_parser.cpp.
#define ACC_INTERFACE 0x0200 |
Definition at line 1831 of file java_bytecode_parser.cpp.
#define ACC_NATIVE 0x0100 |
Definition at line 465 of file java_bytecode_parser.cpp.
#define ACC_PRIVATE 0x0002 |
Definition at line 1823 of file java_bytecode_parser.cpp.
#define ACC_PRIVATE 0x0002 |
Definition at line 1823 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004 |
Definition at line 1824 of file java_bytecode_parser.cpp.
#define ACC_PROTECTED 0x0004 |
Definition at line 1824 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001 |
Definition at line 1822 of file java_bytecode_parser.cpp.
#define ACC_PUBLIC 0x0001 |
Definition at line 1822 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008 |
Definition at line 1825 of file java_bytecode_parser.cpp.
#define ACC_STATIC 0x0008 |
Definition at line 1825 of file java_bytecode_parser.cpp.
#define ACC_STRICT 0x0800 |
Definition at line 468 of file java_bytecode_parser.cpp.
#define ACC_SUPER 0x0020 |
Definition at line 1828 of file java_bytecode_parser.cpp.
#define ACC_SYNCHRONIZED 0x0020 |
Definition at line 463 of file java_bytecode_parser.cpp.
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1833 of file java_bytecode_parser.cpp.
#define ACC_SYNTHETIC 0x1000 |
Definition at line 1833 of file java_bytecode_parser.cpp.
#define ACC_TRANSIENT 0x0080 |
Definition at line 1830 of file java_bytecode_parser.cpp.
#define ACC_VARARGS 0x0080 |
Definition at line 1827 of file java_bytecode_parser.cpp.
#define ACC_VOLATILE 0x0040 |
Definition at line 1829 of file java_bytecode_parser.cpp.
#define CONSTANT_Class 7 |
Definition at line 207 of file java_bytecode_parser.cpp.
#define CONSTANT_Double 6 |
Definition at line 215 of file java_bytecode_parser.cpp.
#define CONSTANT_Fieldref 9 |
Definition at line 208 of file java_bytecode_parser.cpp.
#define CONSTANT_Float 4 |
Definition at line 213 of file java_bytecode_parser.cpp.
#define CONSTANT_Integer 3 |
Definition at line 212 of file java_bytecode_parser.cpp.
#define CONSTANT_InterfaceMethodref 11 |
Definition at line 210 of file java_bytecode_parser.cpp.
#define CONSTANT_InvokeDynamic 18 |
Definition at line 220 of file java_bytecode_parser.cpp.
#define CONSTANT_Long 5 |
Definition at line 214 of file java_bytecode_parser.cpp.
#define CONSTANT_MethodHandle 15 |
Definition at line 218 of file java_bytecode_parser.cpp.
#define CONSTANT_Methodref 10 |
Definition at line 209 of file java_bytecode_parser.cpp.
#define CONSTANT_MethodType 16 |
Definition at line 219 of file java_bytecode_parser.cpp.
#define CONSTANT_NameAndType 12 |
Definition at line 216 of file java_bytecode_parser.cpp.
#define CONSTANT_String 8 |
Definition at line 211 of file java_bytecode_parser.cpp.
#define CONSTANT_Utf8 1 |
Definition at line 217 of file java_bytecode_parser.cpp.
#define T_BOOLEAN 4 |
Definition at line 945 of file java_bytecode_parser.cpp.
#define T_BYTE 8 |
Definition at line 949 of file java_bytecode_parser.cpp.
#define T_CHAR 5 |
Definition at line 946 of file java_bytecode_parser.cpp.
#define T_DOUBLE 7 |
Definition at line 948 of file java_bytecode_parser.cpp.
#define T_FLOAT 6 |
Definition at line 947 of file java_bytecode_parser.cpp.
#define T_INT 10 |
Definition at line 951 of file java_bytecode_parser.cpp.
#define T_LONG 11 |
Definition at line 952 of file java_bytecode_parser.cpp.
#define T_SHORT 9 |
Definition at line 950 of file java_bytecode_parser.cpp.
#define UNUSED_u2 | ( | x | ) | { const u2 x = read_u2(); (void)x; } (void)0 |
Definition at line 473 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_DOUBLE 4 |
Definition at line 226 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_FLOAT 2 |
Definition at line 224 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_INTEGER 1 |
Definition at line 223 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_ITEM_NULL 5 |
Definition at line 227 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_LONG 3 |
Definition at line 225 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_OBJECT 7 |
Definition at line 229 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_TOP 0 |
Definition at line 222 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_UNINIT 8 |
Definition at line 230 of file java_bytecode_parser.cpp.
#define VTYPE_INFO_UNINIT_THIS 6 |
Definition at line 228 of file java_bytecode_parser.cpp.
optionalt<java_bytecode_parse_treet> java_bytecode_parse | ( | const std::string & | file, |
class message_handlert & | msg, | ||
bool | skip_instructions = false |
||
) |
Attempt to parse a Java class from the given file.
file | file to load from |
msg | handles log messages |
skip_instructions | if true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info. |
Definition at line 1890 of file java_bytecode_parser.cpp.
optionalt<java_bytecode_parse_treet> java_bytecode_parse | ( | std::istream & | stream, |
class message_handlert & | msg, | ||
bool | skip_instructions = false |
||
) |
Attempt to parse a Java class from the given stream.
stream | stream to load from |
msg | handles log messages |
skip_instructions | if true, the loaded class's methods will all be empty. Saves time and memory for consumers that only want signature info. |
Definition at line 1870 of file java_bytecode_parser.cpp.