Add tests for Java finally construct

These check that a finally block is accessible when a catch block is
absent, present and catches, present and does not catch, and present
without any exception being thrown at all. The first three cases are
then repeated for the case where an exception escapes from a function
rather than being thrown locally.

Author: smowton

regression/cbmc-java/finally1/test.class

@@ -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.desc

@@ -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.java

@@ -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/finally2/test.class

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

regression/cbmc-java/finally2/test.desc

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

regression/cbmc-java/finally2/test.java

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

regression/cbmc-java/finally3/test.class

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

regression/cbmc-java/finally3/test.desc

@@ -0,0 +1,15 @@
+public class test {
+ public static void main() throws Exception {
+   try {
+     int x = 1;
+     x++;
+   }
+   catch(ArithmeticException e) {
+     assert(false);
+   }
+   finally {
+     assert(false);
+   }
+ }
+}
+

regression/cbmc-java/finally3/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 12: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally4/test.class

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

regression/cbmc-java/finally4/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 12: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/finally4/test.java

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

regression/cbmc-java/finally5/test.class

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

regression/cbmc-java/finally5/test.desc

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