Merge pull request #1813 from smowton/smowton/fix/cleanup-unused-clinits

Java frontend: clean up unused clinit symbols

Author: smowton

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.class

@@ -0,0 +1,22 @@
+public class Test {
+
+  // Refers to, but never instantiates or refers to static fields of, Unused.
+  // Thus a clinit-wrapper for Unused should be created, but subsequently
+  // discarded.
+  Unused u;
+
+  public static void main() {
+
+  }
+
+}
+
+class Unused {
+
+  static int x;
+
+  static {
+    x = 1;
+  }
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Test.java

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--show-goto-functions
+java::Unused::clinit_wrapper
+Unused\.<clinit>\(\)
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/Unused.class

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--lazy-methods --show-goto-functions
+--
+java::Unused::clinit_wrapper
+Unused\.<clinit>\(\)

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--lazy-methods
+VERIFICATION SUCCESSFUL
+

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc

@@ -0,0 +1,26 @@
+public class Test {
+
+  // Refers to, but never instantiates or refers to static fields of, Unused.
+  // Thus a clinit-wrapper for Unused should be created, but subsequently
+  // discarded.
+  Unused1 u;
+
+  public static void main() {
+
+  }
+
+}
+
+class Unused1 extends Unused2 {
+
+}
+
+class Unused2 {
+
+  static int x;
+
+  static {
+    x = 1;
+  }
+
+}