From cd169d6d7c10296f1fbd18560c14d762838d1dc5 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Fri, 11 Aug 2017 14:05:37 +0100
Subject: [PATCH] Add test showing faulty synchronized behaviour

---
 regression/cbmc-java/synchronized/Sync.class | Bin 0 -> 862 bytes
 regression/cbmc-java/synchronized/Sync.java  |  11 +++++++++++
 regression/cbmc-java/synchronized/test.desc  |  10 ++++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc-java/synchronized/Sync.class
 create mode 100644 regression/cbmc-java/synchronized/Sync.java
 create mode 100644 regression/cbmc-java/synchronized/test.desc

diff --git a/regression/cbmc-java/synchronized/Sync.class b/regression/cbmc-java/synchronized/Sync.class
new file mode 100644
index 0000000000000000000000000000000000000000..0c493d5eea9f875453268fe37345d308064aa1ce
GIT binary patch
literal 862
zcmZuuT~E_s6n@^e+q+L0o5K8>V@w?|*bR3Oqat2y(`1AMyz07U6iZ9m&X2#sAK3LY
zfkYEY<j$Yuh5EdJ)I^%*J>SoH&N)ARefb7p6)PE}P)j3;d5L-kI%*ORB_3t)7!8R9
zfl}QJLpz8Z-wR(jq1kusfq>W*NUl4c6Fm{o8w=Y4#)dzz1*Y1LXLm;jeLL7v$pXc;
zZ<+44892(mbQ;l~6B47{`{-F~tUfRuPhh6;roC^zGh43d4O_h^aJ=D~LKg(8{uAns
zT=%u_c#$1!ez5FA#ZSSQ!H}?}Yfy;cD>5<stNy-iMXbvABGY=?F%QqlNz8I`iAAnL
zAhm9}mvd%%{wT2QmyVh$t%$EEupF|;<&Z{3pd6z=`@6QyAn*f$N*ub5Jh>}GiKQHx
zSQaS6`4>bvR_xl^3;g#N`<;rt8!nH<Ee`C^3GBfY1<n_Z7~rLLF~@VKcz#hRE7H_-
z2sH!WJgpX`piC^DKuoA;xWPAh?&N`~t5hbSfN9D!iYU>eijSFXP}W6zX{YnOc{WC>
z+dNx7{RHg@*{{%dPGFplk?2e&Y^<ncnV)43B{ft?Fu{oGS%KuM)2n(VX{Q;LsIh9E
z)D@R1<281_iCfHLXUt%hQlqzw+l<_yRYBr68|V^uCGPQukhuR7M*g`(g=fZts|BpG
hMt#%8<T2zCq%nq}e}?w|G8A+ITJEV@S(S!{xj%2<s1g7G

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/synchronized/Sync.java b/regression/cbmc-java/synchronized/Sync.java
new file mode 100644
index 00000000000..2f8f91cc2ae
--- /dev/null
+++ b/regression/cbmc-java/synchronized/Sync.java
@@ -0,0 +1,11 @@
+public class Sync {
+  public static void main(String[] args) {
+    final Object o = null;
+    try {
+      synchronized (o) {}
+      assert false;
+    } catch (NullPointerException e) {
+      return;
+    }
+  }
+}
diff --git a/regression/cbmc-java/synchronized/test.desc b/regression/cbmc-java/synchronized/test.desc
new file mode 100644
index 00000000000..7155ff81375
--- /dev/null
+++ b/regression/cbmc-java/synchronized/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+Sync.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+See #1236 for details of this test.