From 0c15fed912ff8b7fb465d5532d77e7ba57184986 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Jul 2018 20:05:06 +0100 Subject: [PATCH] Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required --- .../java_bytecode/java_bytecode_parse_tree.h | 52 +++++++------------ .../java_bytecode/java_bytecode_parser.cpp | 4 +- jbmc/src/java_bytecode/java_bytecode_parser.h | 6 ++- 3 files changed, 25 insertions(+), 37 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 431dd4804f5..002c4f615e6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -19,9 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "bytecode_info.h" -class java_bytecode_parse_treet +struct java_bytecode_parse_treet { -public: // Disallow copy construction and copy assignment, but allow move construction // and move assignment. #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported. @@ -32,15 +31,12 @@ class java_bytecode_parse_treet java_bytecode_parse_treet &operator=(java_bytecode_parse_treet &&) = default; #endif - virtual ~java_bytecode_parse_treet() = default; - class annotationt + struct annotationt { - public: typet type; - class element_value_pairt + struct element_value_pairt { - public: irep_idt element_name; exprt value; void output(std::ostream &) const; @@ -58,9 +54,8 @@ class java_bytecode_parse_treet const annotationst &annotations, const irep_idt &annotation_type_name); - class instructiont + struct instructiont { - public: source_locationt source_location; unsigned address; irep_idt statement; @@ -68,17 +63,14 @@ class java_bytecode_parse_treet argst args; }; - class membert + struct membert { - public: std::string descriptor; optionalt signature; irep_idt name; bool is_public, is_protected, is_private, is_static, is_final; annotationst annotations; - virtual void output(std::ostream &out) const = 0; - membert(): is_public(false), is_protected(false), is_private(false), is_static(false), is_final(false) @@ -91,9 +83,8 @@ class java_bytecode_parse_treet } }; - class methodt:public membert + struct methodt : public membert { - public: irep_idt base_name; bool is_native, is_abstract, is_synchronized; source_locationt source_location; @@ -109,7 +100,6 @@ class java_bytecode_parse_treet struct exceptiont { - public: exceptiont() : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt()) { @@ -124,9 +114,8 @@ class java_bytecode_parse_treet typedef std::vector exception_tablet; exception_tablet exception_table; - class local_variablet + struct local_variablet { - public: irep_idt name; std::string descriptor; optionalt signature; @@ -138,9 +127,8 @@ class java_bytecode_parse_treet typedef std::vector local_variable_tablet; local_variable_tablet local_variable_table; - class verification_type_infot + struct verification_type_infot { - public: enum verification_type_info_type { TOP, INTEGER, FLOAT, LONG, DOUBLE, ITEM_NULL, UNINITIALIZED_THIS, OBJECT, UNINITIALIZED}; @@ -150,9 +138,8 @@ class java_bytecode_parse_treet u2 offset; }; - class stack_map_table_entryt + struct stack_map_table_entryt { - public: enum stack_frame_type { SAME, SAME_LOCALS_ONE_STACK, SAME_LOCALS_ONE_STACK_EXTENDED, @@ -175,7 +162,7 @@ class java_bytecode_parse_treet typedef std::vector stack_map_tablet; stack_map_tablet stack_map_table; - virtual void output(std::ostream &out) const; + void output(std::ostream &out) const; methodt(): is_native(false), @@ -183,21 +170,21 @@ class java_bytecode_parse_treet is_synchronized(false) { } - - virtual ~methodt() = default; }; - class fieldt:public membert + struct fieldt : public membert { - public: - virtual ~fieldt() = default; - virtual void output(std::ostream &out) const; bool is_enum; + + void output(std::ostream &out) const; + + fieldt() : is_enum(false) + { + } }; - class classt + struct classt { - public: classt() = default; // Disallow copy construction and copy assignment, but allow move @@ -230,9 +217,8 @@ class java_bytecode_parse_treet }; typedef std::vector u2_valuest; - class lambda_method_handlet + struct lambda_method_handlet { - public: method_handle_typet handle_type; irep_idt lambda_method_name; irep_idt lambda_method_ref; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 82c66bf5c5e..5585ee21bf3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1779,7 +1779,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class) rmethod_attribute(method); } -optionalt +optionalt java_bytecode_parse(std::istream &istream, message_handlert &message_handler) { java_bytecode_parsert java_bytecode_parser; @@ -1796,7 +1796,7 @@ java_bytecode_parse(std::istream &istream, message_handlert &message_handler) return std::move(java_bytecode_parser.parse_tree); } -optionalt +optionalt java_bytecode_parse(const std::string &file, message_handlert &message_handler) { std::ifstream in(file, std::ios::binary); diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.h b/jbmc/src/java_bytecode/java_bytecode_parser.h index f723f8bf197..8a2304f219e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.h +++ b/jbmc/src/java_bytecode/java_bytecode_parser.h @@ -14,10 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -optionalt +struct java_bytecode_parse_treet; + +optionalt java_bytecode_parse(const std::string &file, class message_handlert &); -optionalt +optionalt java_bytecode_parse(std::istream &, class message_handlert &); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H