From f8511c2358d2d484d3140cab8e7e6ec27e74a020 Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 12 Feb 2020 10:33:59 -0800
Subject: [PATCH] [topl] Added another small test, for BAOS.

Summary:
This adds a violation of baos.topl found in github/seata/seata. However,
it is not a bug (see comment in commit).

Reviewed By: ngorogiannis

Differential Revision: D19518641

fbshipit-source-id: e219245ee
---
 .../java/topl/baos/BaosTest.java              | 24 +++++++++++++++----
 .../codetoanalyze/java/topl/baos/issues.exp   |  1 +
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
index 5a08ef7f6..b661c95d1 100644
--- a/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
+++ b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
@@ -8,9 +8,10 @@ import java.io.ByteArrayOutputStream;
 import java.io.DataOutputStream;
 import java.io.IOException;
 import java.io.ObjectOutputStream;
+import java.util.zip.GZIPOutputStream;
 
 class BaosTest {
-  void aBad() throws IOException {
+  static void aBad() throws IOException {
     ByteArrayOutputStream x = new ByteArrayOutputStream();
     ObjectOutputStream y = new ObjectOutputStream(x);
     y.writeObject(1337);
@@ -18,7 +19,7 @@ class BaosTest {
   }
 
   /** Bugfix for aBad. */
-  void a1Ok() throws IOException {
+  static void a1Ok() throws IOException {
     ByteArrayOutputStream x = new ByteArrayOutputStream();
     ObjectOutputStream y = new ObjectOutputStream(x);
     y.writeObject(1337);
@@ -27,7 +28,7 @@ class BaosTest {
   }
 
   /** Another bugfix for aBad. */
-  void a2Ok() throws IOException {
+  static void a2Ok() throws IOException {
     ByteArrayOutputStream x = new ByteArrayOutputStream();
     ObjectOutputStream y = new ObjectOutputStream(x);
     y.writeObject(1337);
@@ -35,7 +36,7 @@ class BaosTest {
     byte[] bytes = x.toByteArray();
   }
 
-  void bBad() throws IOException {
+  static void bBad() throws IOException {
     ByteArrayOutputStream x = new ByteArrayOutputStream();
     ObjectOutputStream y = new ObjectOutputStream(x);
     y.writeObject(1337);
@@ -43,10 +44,23 @@ class BaosTest {
     y.close();
   }
 
-  void cBad() throws IOException {
+  static void cBad() throws IOException {
     ByteArrayOutputStream x = new ByteArrayOutputStream();
     DataOutputStream y = new DataOutputStream(x);
     y.writeLong(1337);
     byte[] bytes = x.toByteArray();
   }
+
+  /**
+   * This false positive is caused by the property being imprecise. However, it is also an example
+   * where, arguably, GZIPOutputStream breaks the behavioral contract on OutputStream: it may be
+   * surprising that finish() sends data to the underlying stream but flush() may not.
+   */
+  static byte[] FP_dOk(final byte[] src) throws IOException {
+    ByteArrayOutputStream x = new ByteArrayOutputStream(src.length);
+    GZIPOutputStream y = new GZIPOutputStream(x);
+    y.write(src);
+    y.finish();
+    return x.toByteArray();
+  }
 }
diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp
index f1e08c7e0..02a4cefe4 100644
--- a/infer/tests/codetoanalyze/java/topl/baos/issues.exp
+++ b/infer/tests/codetoanalyze/java/topl/baos/issues.exp
@@ -1,3 +1,4 @@
+codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, []
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
 codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []