From 7cdd2e2777ff0e1fb122dc3498c3d91cca8abfdd Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 18 Sep 2019 16:19:37 +0100
Subject: [PATCH] Add regression test for --assert-no-exceptions-thrown

This tests the option behaves as desired.
---
 .../MyException.class                         | Bin 0 -> 192 bytes
 .../assert-no-exceptions-thrown/Test.class    | Bin 0 -> 964 bytes
 .../assert-no-exceptions-thrown/Test.java     |  33 ++++++++++++++++++
 .../test-with-throw.desc                      |  14 ++++++++
 .../assert-no-exceptions-thrown/test.desc     |  18 ++++++++++
 5 files changed, 65 insertions(+)
 create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class
 create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class
 create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java
 create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc
 create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc

diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class
new file mode 100644
index 0000000000000000000000000000000000000000..5578fa11a8f315cee834ac189ccca4cbadae3b8c
GIT binary patch
literal 192
zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;|
zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSN!0lV<T9KSuP?DLS
z$H*WIlF`pe%uCmYi!vxMFahla0Y)GO>H^YiK$a|!28pn0ZD(NI2$p6Cl5Ai>kQ4`y
I$Hc%105{kpi2wiq

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..9b30d4d418e8e5e87211093334a7f249582c8833
GIT binary patch
literal 964
zcmZWnOHUJF6g^)%4?3NeQWS@lw}?QM8q>H!QbbHlco-lgvYSr7$UteybgJ-ISh4Gd
z4VsA2ME3p?e}gf`^9_$GZ0_qjbI-Z=&W}G|zXK?tXd#VJ6Jr))%HOx3DL-z(z^DZq
z4-zyJCLUU_)XSuWDNLIv2=tD-&87@Ozfo_#^qX#_CaVHsOTd`*>wY*V5TBgd6wnqL
zRVmQD<k#g&Yp)`M4FwkH+H(&#wu8n8VkQ@+UJInwL)Y6~cK0t4*5ZLD_ah1c-P@Ml
z?ge&}VyT-_*=E+OT@qUBjaJ~vSH5bW*pSU|X2*T++UP-6U`WNqnp=NYTxr#6ZyJ6*
zl)*KHKyvx;pRBh7k5nqrHtwR&MmI77PUn68Y7>h=&<H3|QJZ*V<1uCgG9Bb<Wk-4;
zx6vsr)VN52zN&2cfvjHl;x57#AGpOWjPed?9!+E%#m-2BP-D^dG8?29^!oG}#Hj+}
z4y_Rt<47poJhFlw&?{&um#H5k`3<qRXNaHYGG3Hv%yed9lo`xSX2CIZ{X{$Acd@AR
z1bdQ>3<iantaV|4wK4uE(@5e81wZA>J)#U~=~T*u!&u2Si0em=k<#;%9b@#B+!x+5
zuOFl5BN9hSnML;Gd0x9!YUA0`|DZO;Z&k84DyN8(r+^u%P`(`T7O+M|7gNn~x!^21
z_hoTo4)qVx7BI}O`cb6n=Zwq9W1jP_GF~HM9Yb(25>4x%>o*+n3)vSY@@bj@Wd_sS
r(9re4O3@8~o~->DsUw(L8(RDm66$ytVy=#-R;VLpm(_`fqvw&ob0Vyk

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java
new file mode 100644
index 0000000000..ed234bf44a
--- /dev/null
+++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java
@@ -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;
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc
new file mode 100644
index 0000000000..d3f015b3f8
--- /dev/null
+++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc
@@ -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.
diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc
new file mode 100644
index 0000000000..9b6f000e11
--- /dev/null
+++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc
@@ -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.