Merge pull request #1230 from reuk/reuk/synchronized-test

Add test showing faulty synchronized behaviour

Author: thk123

regression/cbmc-java/synchronized/Sync.class

@@ -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;
+    }
+  }
+}

regression/cbmc-java/synchronized/Sync.java

@@ -0,0 +1,10 @@
+KNOWNBUG
+Sync.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+See #1236 for details of this test.