Added more regression tests for runtime exceptions

Author: cristina-david

regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java

@@ -1,14 +1,14 @@
 public class ArrayIndexOutOfBoundsExceptionTest {
     public static void main(String args[]) {
-	try {
-	    int[] a=new int[4];
-	    a[6]=0;
-	    // TODO: fix the bytecode convertion such that there is no need for
-	    // an explicit throw in order to convert the handler
-	    throw new RuntimeException();
-	}
-	catch(ArrayIndexOutOfBoundsException exc) {
-	    assert false;
-	}
+        try {
+            int[] a=new int[4];
+            a[6]=0;
+            // TODO: fix the bytecode convertion such that there is no need for
+            // an explicit throw in order to convert the handler
+            throw new RuntimeException();
+        }
+        catch(ArrayIndexOutOfBoundsException exc) {
+            assert false;
+        }
     }
 }

regression/cbmc-java/ClassCastException1/A.class

@@ -0,0 +1,21 @@
+class A {
+  int i;
+}
+
+class B {
+  int j;
+}
+
+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/B.class

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

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class

@@ -0,0 +1,21 @@
+class A {
+  int i;
+}
+
+class B {
+  int j;
+}
+
+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/ClassCastExceptionTest.java

@@ -0,0 +1,9 @@
+CORE
+ClassCastExceptionTest.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*Dynamic cast check: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException1/test.desc

@@ -1,11 +1,11 @@
 public class NegativeArraySizeExceptionTest {
   public static void main(String args[]) {
       try {
-	  int a[]=new int[-1];
-	  throw new RuntimeException();
+          int a[]=new int[-1];
+          throw new RuntimeException();
       }
       catch (NegativeArraySizeException exc) {
-	  assert false;
+          assert false;
       }
   }
 }

regression/cbmc-java/ClassCastException2/A.class

@@ -6,13 +6,13 @@ class A {
 
 public class Test {
     public static void main(String args[]) {
-	A a=null;
-	try {
-	    int i=a.i;
-	    throw new B();
-	}
-	catch (NullPointerException exc) {
-	    assert false;
-	}
+        A a=null;
+        try {
+            int i=a.i;
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
     }
 }

regression/cbmc-java/ClassCastException2/B.class

@@ -0,0 +1,18 @@
+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;
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*reference is null in \*a: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring