Test assert-no-exceptions-thrown and runtime exception

Test that when both are combined, --throw-runtime-exception still
works.

Author: romainbrenguier

jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class

@@ -0,0 +1,54 @@
+public class Thrower {
+  public static void test(Integer t) {
+    String ret = "";
+    if (t != null)
+      try {
+        switch (t) {
+        case 1:
+          ret = "CCE";
+          Object o = new Integer(0);
+          String x = ((String) o);
+          break;
+
+        case 2:
+          ret = "AIOBE";
+          int[] xs = new int[3];
+          t = xs[5];
+
+        case 3:
+          ret = "AE";
+          t = 5 / 0;
+
+        case 4:
+          ret = "NASE";
+          Integer[] arr = new Integer[-7];
+
+        case 5:
+          ret = "NPE";
+          String str = null;
+          str.toLowerCase();
+          
+        default:
+          break;
+        }
+      } catch (ClassCastException | NegativeArraySizeException
+               | NullPointerException | ArithmeticException
+               | ArrayIndexOutOfBoundsException e3) {
+
+        if (e3 instanceof ClassCastException)
+          assert ret.equals("CCE");
+
+        if (e3 instanceof NegativeArraySizeException)        
+          assert ret.equals("NASE");
+
+        if (e3 instanceof NullPointerException)
+          assert ret.equals("NPE");
+       
+        if (e3 instanceof ArithmeticException)
+          assert ret.equals("AE");
+
+        if (e3 instanceof ArrayIndexOutOfBoundsException)
+          assert ret.equals("AIOBE");
+      }
+  }
+}

jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java

@@ -0,0 +1,14 @@
+CORE
+Thrower.class
+--function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions
+line 39 assertion at file Thrower.java line 39 .*: FAILURE
+line 42 assertion at file Thrower.java line 42 .*: FAILURE
+line 45 assertion at file Thrower.java line 45 .*: FAILURE
+line 48 assertion at file Thrower.java line 48 .*: FAILURE
+line 51 assertion at file Thrower.java line 51 .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that the runtime exceptions still throw with `--throw-runtime-exceptions`
+even when `--assert-no-exceptions-thrown` is specified.