Fixes to exception handling behaviour

Corrected the ordering of exception catching and added tests to verify the
correct behaviour.  Previously, the universal catch would be the one on the
outermost try (should be the innermost try).
Also, a throw can never throw directly past this catch, so there is no need to
include these alternatives (they will appear in the rethrow of the finally).

Author: dcattaruzza

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