Added regression tests

Author: NathanJPhillips

regression/cbmc-java/overlay-class/Test.class

@@ -0,0 +1,14 @@
+public class Test
+{
+  public int x;
+
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+
+  public static void notOverlain()
+  {
+    assert(true);
+  }
+}

regression/cbmc-java/overlay-class/Test.java

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayClassImplementation {
+}

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.class

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayMethodImplementation {
+}

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java

@@ -0,0 +1,14 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+@OverlayClassImplementation
+public class Test
+{
+  public int x;
+
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(true);
+  }
+}

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.class

@@ -0,0 +1,17 @@
+CORE
+Test.class
+`./format_classpath.sh . annotations correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java

@@ -0,0 +1,17 @@
+CORE
+Test.class
+`./format_classpath.sh . annotations . correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$

regression/cbmc-java/overlay-class/correct-overlay/Test.class

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+unameOut="$(uname -s)"
+case "${unameOut}" in
+    CYGWIN*)    separator=";";;
+    MINGW*)     separator=";";;
+    MSYS*)      separator=";";;
+    Windows*)   separator=";";;
+    *)          separator=":"
+esac
+
+echo -n "--classpath \""
+echo -n `IFS=$separator; echo "$*"`
+echo -n "\""

regression/cbmc-java/overlay-class/correct-overlay/Test.java

@@ -0,0 +1,16 @@
+CORE
+Test.class
+`./format_classpath.sh annotations correct-overlay .` --verbosity 10
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol:  field 'x'$
+^Adding symbol:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class

regression/cbmc-java/overlay-class/correct-test.desc

@@ -0,0 +1,11 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+public class Test
+{
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+}

regression/cbmc-java/overlay-class/duplicate-test.desc

@@ -0,0 +1,16 @@
+CORE
+Test.class
+`./format_classpath.sh . annotations unmarked-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol:  field 'x'$
+^Adding symbol:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class