Merge pull request #1196 from smowton/smowton/fix/exception_catch

Implement exception catching

Author: smowton

regression/cbmc-java/exceptions22/test.class

@@ -0,0 +1,11 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
+--
+This test checks that a thrown exception is caught, and is not erroneously rethrown
+on function exit such that another surrounding try block can catch it again.

regression/cbmc-java/exceptions22/test.desc

@@ -0,0 +1,20 @@
+public class test {
+  public static void main () {
+    try {
+      f();
+    }
+    catch(Exception e) {
+      assert(false); // Should be unreachable
+    }
+  }
+
+  public static void f() {
+    try {
+      throw new Exception();
+    }
+    catch(Exception e) {
+      // Should prevent main's catch handler from being invoked
+    }
+  }
+}
+

regression/cbmc-java/exceptions22/test.java

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally1/test.class

@@ -0,0 +1,11 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     throw new Exception();
+   }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally1/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally1/test.java

@@ -0,0 +1,12 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     throw new Exception();
+   }
+   catch(Exception e) { }
+   finally {
+     assert(false);
+   }
+ }
+}
+