Add regression test for --assume-no-throw-exceptions

This tests the option behaves as desired.

Author: romainbrenguier

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

@@ -0,0 +1,36 @@
+class MyException extends Exception {}
+
+public class Test {
+  public static int mayThrow(String branch) throws Throwable {
+    if (branch == null) {
+      return -1;
+    }
+    if (branch.startsWith("null pointer exception")) {
+      throw new NullPointerException();
+    } else if (branch.startsWith("custom exception")) {
+      throw new MyException();
+    } else if (branch.startsWith("throwable")) {
+      throw new Throwable();
+    } else if (branch.startsWith("return 2")) {
+      return 2;
+    } else {
+      return 1;
+    }
+  }
+
+  public static void check(String 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/assume-no-exceptions-thrown/Test.class

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.check
+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
+line 32 assertion at file Test.java line 32 .*: FAILURE
+line 34 assertion at file Test.java line 34 .*: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that we get the expected behaviour when --assume-no-exceptions-thrown is
+not used. This is to make sure that test.desc is actually testing what we wanted.

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

@@ -0,0 +1,18 @@
+CORE
+Test.class
+--function Test.check --assume-no-exceptions-thrown
+line 10 assertion at file Test.java line 10 .*: FAILURE
+line 12 assertion at file Test.java line 12 .*: FAILURE
+line 14 assertion at file Test.java line 14 .*: 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 .*: SUCCESS
+line 32 assertion at file Test.java line 32 .*: SUCCESS
+line 34 assertion at file Test.java line 34 .*: 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.