From c14e907c331f47429cbd488b3421485e4085a4f4 Mon Sep 17 00:00:00 2001
From: johndumbell <john.dumbell@diffblue.com>
Date: Fri, 23 Mar 2018 10:49:01 +0000
Subject: [PATCH 1/3] Increase AssertionError arguments allowed from 2 to 3

There is a constructor for this class with 2 arguments plus implied this.
---
 src/goto-programs/builtin_functions.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 35e67c16b5e..c7cfe83fda4 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -969,11 +969,11 @@ void goto_convertt::do_function_call_symbol(
 
     copy(function_call, FUNCTION_CALL, dest);
 
-    if(arguments.size()!=1 && arguments.size()!=2)
+    if(arguments.size() != 1 && arguments.size() != 2 && arguments.size() != 3)
     {
       error().source_location=function.find_source_location();
       error() << "`" << identifier
-              << "' expected to have one or two arguments" << eom;
+              << "' expected to have one, two or three arguments" << eom;
       throw 0;
     }
 

From eea76ece5628a1abcd67052daa14d2d536774d4e Mon Sep 17 00:00:00 2001
From: johndumbell <john.dumbell@diffblue.com>
Date: Wed, 11 Apr 2018 15:59:53 +0100
Subject: [PATCH 2/3] Add a regression test.

---
 .../AssertionIssue.class                          | Bin 0 -> 556 bytes
 .../AssertionIssue.java                           |  13 +++++++++++++
 .../assertion_error_constructors/test.desc        |   8 ++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc-java/assertion_error_constructors/AssertionIssue.class
 create mode 100644 regression/cbmc-java/assertion_error_constructors/AssertionIssue.java
 create mode 100644 regression/cbmc-java/assertion_error_constructors/test.desc

diff --git a/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class
new file mode 100644
index 0000000000000000000000000000000000000000..a9312303951fc670042fcc5d3a7346dcfd005cda
GIT binary patch
literal 556
zcmZWmO;5r=5Pb`ULPg|56h8xr2jBn)j~Ej}G$Cp903qSn;s%zKZL%#Af0ic_N%ZcI
zGR{_0H11($=gph<cG{26*Eax{IJ1yJ#l%4dhbF2P3{)&6aAe}x#0f)bI8*-0aXo$$
z1YCu}mkhbSlw9>ZhoFEVeI=v_uNjh!=7_=Q`H!4o&lZy3FBdLXLp@Jgwm)&ak)wpJ
ze?TLg3DPLov3@@Ymb}Z554Cj+Ggt$EsV4kRXt8qKi1_Wf^W@~PgB(Lu-#eZor=6H|
ztCX)8&IkU2lcSv0R$PX)kSirz@42>8zMQrh>hVM*d+~pLZE{Ml`%9z^wyqEEoKHfA
zR>R(cgHVxe_ZJdtcbg;BVbZVACjqASptws_hccs_YOTRuqIRBQIs)k{(_K@EfC7q?
vvna*GO+xi4Zjcz4k{cM~HBxJ&-wC80D1HkW<XWaGfqht%E$SNdqAapssCa?e

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java
new file mode 100644
index 00000000000..b82d7b46df3
--- /dev/null
+++ b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java
@@ -0,0 +1,13 @@
+public class AssertionIssue {
+
+    public static void throwAssertion() {
+        throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
+    }
+
+    public static class ThrowableAssertion extends Throwable {
+        @Override
+        public String getMessage() {
+            return "How did we get here?";
+        }
+    }
+}
diff --git a/regression/cbmc-java/assertion_error_constructors/test.desc b/regression/cbmc-java/assertion_error_constructors/test.desc
new file mode 100644
index 00000000000..c5b41d9ba22
--- /dev/null
+++ b/regression/cbmc-java/assertion_error_constructors/test.desc
@@ -0,0 +1,8 @@
+CORE
+AssertionIssue.class
+--function AssertionIssue.throwAssertion
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 97d556ecfe573c07f39f3e9aa36bf9bee0d7b919 Mon Sep 17 00:00:00 2001
From: johndumbell <john.dumbell@diffblue.com>
Date: Wed, 11 Apr 2018 16:54:01 +0100
Subject: [PATCH 3/3] Update desc file to add pass variables.

---
 regression/cbmc-java/assertion_error_constructors/test.desc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc-java/assertion_error_constructors/test.desc b/regression/cbmc-java/assertion_error_constructors/test.desc
index c5b41d9ba22..fde9624618f 100644
--- a/regression/cbmc-java/assertion_error_constructors/test.desc
+++ b/regression/cbmc-java/assertion_error_constructors/test.desc
@@ -1,8 +1,8 @@
 CORE
 AssertionIssue.class
 --function AssertionIssue.throwAssertion
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 ^warning: ignoring