Add regression test for runtime exceptions instrumentation

Author: cristina-david

regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class

@@ -0,0 +1,12 @@
+public class ArrayIndexOutOfBoundsExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int[] a=new int[4];
+          a[4]=0;
+          throw new RuntimeException();
+      }
+      catch (ArrayIndexOutOfBoundsException exc) {
+          assert false;
+      }
+  }
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java

@@ -0,0 +1,9 @@
+CORE
+ArrayIndexOutOfBoundsExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc

@@ -0,0 +1,13 @@
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          Object x = new Integer(0);
+          String y = (String)x;
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+    
+  }
+}

regression/cbmc-java/ClassCastException1/A.class

@@ -0,0 +1,9 @@
+CORE
+ClassCastExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ClassCastExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException1/B.class

@@ -0,0 +1,21 @@
+class A {}
+
+class B extends A {}
+
+class C extends B {}
+
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          A c = new C();
+          B b = (B)c;
+          // TODO: an explicit throw is currently needed in order
+          // for CBMC to convert the exception handler
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+    
+  }
+}

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class

@@ -0,0 +1,8 @@
+CORE
+ClassCastExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java

@@ -0,0 +1,20 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            a.i=0;
+            // TODO: an explicit throw is currently needed in order
+            // for CBMC to convert the exception handler
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ClassCastException1/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file Test.java line 15 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException2/A.class

@@ -0,0 +1,20 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            int i=a.i;
+            // TODO: an explicit throw is currently needed in order
+            // for CBMC to convert the exception handler
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ClassCastException2/B.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file Test.java line 15 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring