Add regression test for --assert-no-exceptions-thrown

This tests the option behaves as desired.

Author: romainbrenguier

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

@@ -0,0 +1,33 @@
+class MyException extends Exception {}
+
+public class Test {
+  public static int mayThrow(char branch) throws Throwable {
+    if (branch == 'n') {
+      throw new NullPointerException();
+    } else if (branch == 'c') {
+      throw new MyException();
+    } else if (branch == 't') {
+      throw new Throwable();
+    } else if (branch == 'r') {
+      return 2;
+    } else {
+      return 1;
+    }
+  }
+
+  public static void check(char branch) {
+    try {
+      int i = mayThrow(branch);
+      if (i == 2)
+        assert false;
+      if (i == 1)
+        assert false;
+    } catch (MyException e) {
+      assert false;
+    } catch (NullPointerException e) {
+      assert false;
+    } catch (Throwable e) {
+      assert false;
+    }
+  }
+}

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

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.check
+line 22 assertion at file Test.java line 22 .*: FAILURE
+line 24 assertion at file Test.java line 24 .*: FAILURE
+line 26 assertion at file Test.java line 26 .*: FAILURE
+line 28 assertion at file Test.java line 28 .*: FAILURE
+line 30 assertion at file Test.java line 30 .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that we get the expected behaviour when --assert-no-exceptions-thrown is
+not used. This is to make sure that test.desc is actually testing what we wanted.

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

@@ -0,0 +1,18 @@
+CORE
+Test.class
+--function Test.check --assert-no-exceptions-thrown
+line 6 assertion at file Test.java line 6 .*: FAILURE
+line 8 assertion at file Test.java line 8 .*: FAILURE
+line 10 assertion at file Test.java line 10 .*: FAILURE
+line 22 assertion at file Test.java line 22 .*: FAILURE
+line 24 assertion at file Test.java line 24 .*: FAILURE
+line 26 assertion at file Test.java line 26 .*: SUCCESS
+line 28 assertion at file Test.java line 28 .*: SUCCESS
+line 30 assertion at file Test.java line 30 .*: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that the `throw` instructions have been replaced by assertions, which
+are failing here because they are reachable, and assumptions which prevent
+the last three assertions from failing.