Merge pull request diffblue#2564 from tautschnig/vs-java-parse-tree

Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -19,9 +19,8 @@ Author: Daniel Kroening, [email protected]
 
 #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,27 +54,23 @@ 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;
     typedef std::vector<exprt> argst;
     argst args;
   };
 
-  class membert
+  struct membert
   {
-  public:
     std::string descriptor;
     optionalt<std::string> 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<exceptiont> exception_tablet;
     exception_tablet exception_table;
 
-    class local_variablet
+    struct local_variablet
     {
-    public:
       irep_idt name;
       std::string descriptor;
       optionalt<std::string> signature;
@@ -138,9 +127,8 @@ class java_bytecode_parse_treet
     typedef std::vector<local_variablet> 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,29 +162,29 @@ class java_bytecode_parse_treet
     typedef std::vector<stack_map_table_entryt> 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),
       is_abstract(false),
       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> 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;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1775,7 +1775,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
     rmethod_attribute(method);
 }
 
-optionalt<class java_bytecode_parse_treet>
+optionalt<java_bytecode_parse_treet>
 java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
 {
   java_bytecode_parsert java_bytecode_parser;
@@ -1792,7 +1792,7 @@ java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
   return std::move(java_bytecode_parser.parse_tree);
 }
 
-optionalt<class java_bytecode_parse_treet>
+optionalt<java_bytecode_parse_treet>
 java_bytecode_parse(const std::string &file, message_handlert &message_handler)
 {
   std::ifstream in(file, std::ios::binary);

jbmc/src/java_bytecode/java_bytecode_parser.h

@@ -14,10 +14,12 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <util/optional.h>
 
-optionalt<class java_bytecode_parse_treet>
+struct java_bytecode_parse_treet;
+
+optionalt<java_bytecode_parse_treet>
 java_bytecode_parse(const std::string &file, class message_handlert &);
 
-optionalt<class java_bytecode_parse_treet>
+optionalt<java_bytecode_parse_treet>
 java_bytecode_parse(std::istream &, class message_handlert &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H