Merge pull request #1725 from cesaro/exception-handlig-fixes

Exception handling fixes

Author: tautschnig

regression/cbmc-java/exceptions26/A.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test verifies that catches are executed in the correct order
+

regression/cbmc-java/exceptions26/B.class

@@ -0,0 +1,31 @@
+class A extends RuntimeException {}
+class B extends A {}
+
+// This test verifies that catches are executed in the correct order
+public class test {
+  public static void main (String args[]) {
+    int i = 0;
+    try {
+      try {
+        throw new A();
+      }
+      catch(A exc) {
+        i++;
+        throw new B();
+      }
+      finally
+      {
+        // Make sure A threw into the catch
+        assert(i==1);
+        i++;
+      }
+    }
+    catch(B exc) {
+      // Make sure finally was executed
+      assert(i==2);
+      i++;
+    }
+    // Make sure B was rethrown by finally
+    assert(i==3);
+  }
+}

regression/cbmc-java/exceptions26/test.class

@@ -0,0 +1,7 @@
+CORE
+test.class
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
+--
+Tests embedded try-catch-finally to ensure the catching order is correct

regression/cbmc-java/exceptions26/test.desc

@@ -0,0 +1,54 @@
+import org.cprover.CProver;
+class A extends RuntimeException {}
+class B extends A {}
+
+// This test verifies that catches are executed in the correct order
+public class test {
+  public static void main (String args[]) {
+    int i = 0;
+    int j = 0;
+    try {
+      try {
+        try {
+          if (CProver.nondetBoolean()) throw new A();
+          else throw new B();
+        }
+        catch(B exc) {
+          i++;
+        }
+        catch(A exc) {
+          i++;
+          throw new B();
+        }
+        finally
+        {
+          // Make sure A threw into the catch
+          assert(i==1);
+          i++;
+        }
+        assert(i==2);
+        // Account for the rethrow in finally
+        j++;
+      }
+      catch(B exc) {
+        // Make sure finally was executed
+        assert(i==2);
+        i++;
+        throw new B();
+      }
+      finally 
+      {
+        assert ((i+j) == 3);
+      }
+      // Account for the rethrow in finally
+      j++;
+    }
+    catch(B exc)
+    {
+      i++;
+    }
+    // Make sure B was rethrown by finally when A was thrown
+    // or if B was thrown there was no rethrow
+    assert(i+j == 4);
+  }
+}