From 6c0c8d9e60450fef113a9eb27a9c417605d37ecd Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 3 May 2018 22:17:22 +0100
Subject: [PATCH 1/2] pretty print constructor names, in the style of javap

---
 .../java_bytecode_parse_tree.cpp              | 28 ++++++++++---------
 src/java_bytecode/java_bytecode_parse_tree.h  | 20 +++++++++++--
 2 files changed, 32 insertions(+), 16 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp
index 5b73a88e911..602bf93b71e 100644
--- a/src/java_bytecode/java_bytecode_parse_tree.cpp
+++ b/src/java_bytecode/java_bytecode_parse_tree.cpp
@@ -63,22 +63,16 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const
     out << " extends " << extends;
   out << " {" << '\n';
 
-  for(fieldst::const_iterator
-      it=fields.begin();
-      it!=fields.end();
-      it++)
+  for(const auto &f : fields)
   {
-    it->output(out);
+    f.output(name, out);
   }
 
   out << '\n';
 
-  for(methodst::const_iterator
-      it=methods.begin();
-      it!=methods.end();
-      it++)
+  for(const auto &m : methods)
   {
-    it->output(out);
+    m.output(name, out);
   }
 
   out << '}' << '\n';
@@ -139,7 +133,9 @@ bool java_bytecode_parse_treet::does_annotation_exist(
       }) != annotations.end();
 }
 
-void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
+void java_bytecode_parse_treet::methodt::output(
+  const irep_idt &class_name,
+  std::ostream &out) const
 {
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
@@ -174,7 +170,11 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
   if(is_synchronized)
     out << "synchronized ";
 
-  out << name;
+  if(is_constructor())
+    out << class_name;
+  else
+    out << name;
+
   out << " : " << descriptor;
 
   out << '\n';
@@ -218,7 +218,9 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
   out << '\n';
 }
 
-void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
+void java_bytecode_parse_treet::fieldt::output(
+  const irep_idt &class_name,
+  std::ostream &out) const
 {
   for(const auto &annotation : annotations)
   {
diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h
index 7e583af3673..c7673cc50dc 100644
--- a/src/java_bytecode/java_bytecode_parse_tree.h
+++ b/src/java_bytecode/java_bytecode_parse_tree.h
@@ -67,7 +67,9 @@ class java_bytecode_parse_treet
     bool is_public, is_protected, is_private, is_static, is_final;
     annotationst annotations;
 
-    virtual void output(std::ostream &out) const = 0;
+    virtual void output(
+      const irep_idt &class_name,
+      std::ostream &out) const = 0;
 
     membert():
       is_public(false), is_protected(false),
@@ -80,6 +82,12 @@ class java_bytecode_parse_treet
   {
   public:
     irep_idt base_name;
+
+    bool is_constructor() const
+    {
+      return base_name=="<init>";
+    }
+
     bool is_native, is_abstract, is_synchronized;
     source_locationt source_location;
 
@@ -155,7 +163,9 @@ 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(
+      const irep_idt &class_name,
+      std::ostream &out) const override;
 
     methodt():
       is_native(false),
@@ -171,7 +181,11 @@ class java_bytecode_parse_treet
   {
   public:
     virtual ~fieldt() = default;
-    virtual void output(std::ostream &out) const;
+
+    void output(
+      const irep_idt &class_name,
+      std::ostream &out) const override;
+
     bool is_enum;
   };
 

From ab7817962204962bb1a141935d84a3aead9237c1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 3 May 2018 22:19:47 +0100
Subject: [PATCH 2/2] use is_constructor member in parse tree

---
 src/java_bytecode/java_bytecode_convert_method.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 9b221d4298c..e92b88bc33a 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -354,6 +354,7 @@ void java_bytecode_convert_method_lazy(
   method_symbol.mode=ID_java;
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
+
   if(m.is_public)
     member_type.set_access(ID_public);
   else if(m.is_protected)
@@ -363,7 +364,7 @@ void java_bytecode_convert_method_lazy(
   else
     member_type.set_access(ID_default);
 
-  if(is_constructor(method_symbol.base_name))
+  if(m.is_constructor())
   {
     method_symbol.pretty_name=
       id2string(class_symbol.pretty_name)+"."+
@@ -563,7 +564,7 @@ void java_bytecode_convert_methodt::convert(
   // The pretty name of a constructor includes the base name of the class
   // instead of the internal method name "<init>". For regular methods, it's
   // just the base name of the method.
-  if(is_constructor(method_symbol.base_name))
+  if(m.is_constructor())
   {
     method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
                                 id2string(class_symbol.base_name) + "()";