Add tests to verify that synthetic method removal is performed

These check that direct and indirect clinit wrappers, as well as stub class synthetic
static initialisers, are removed if they are generated but not subsequently called.

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;
+  }
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.class

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Test.java

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused1.class

@@ -0,0 +1,22 @@
+public class Test {
+
+  public static void main() {
+
+  }
+
+  public static Opaque unused() {
+
+    // Should cause jbmc to create a synthetic static initialiser for Opaque,
+    // but because this function isn't called by main() it should then be
+    // cleaned up as unused.
+    return Opaque.field;
+
+  }
+
+}
+
+class Opaque {
+
+  public static Opaque field;
+
+}

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/Unused2.class

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc

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