From bfdb379fe39573c7e34322503d281c81a4a38dfb Mon Sep 17 00:00:00 2001
From: Radu Grigore <rgrigore@fb.com>
Date: Wed, 15 Jan 2020 10:42:14 -0800
Subject: [PATCH] [topl] Added a test, for intraprocedural reasoning.

Summary:
The property SkipAfterRemove already had a test, but not for
intra-procedural violations. This adds a test for that case.

Reviewed By: ngorogiannis

Differential Revision: D19330471

fbshipit-source-id: 1dd1c3ad7
---
 .../java/topl/skip/IndirectSkip.java          | 35 +++++++++++++++++++
 .../codetoanalyze/java/topl/skip/Makefile     |  2 +-
 .../java/topl/skip/SkipAfterRemove.topl       |  2 +-
 .../codetoanalyze/java/topl/skip/issues.exp   |  2 ++
 4 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/java/topl/skip/IndirectSkip.java

diff --git a/infer/tests/codetoanalyze/java/topl/skip/IndirectSkip.java b/infer/tests/codetoanalyze/java/topl/skip/IndirectSkip.java
new file mode 100644
index 000000000..1713c8351
--- /dev/null
+++ b/infer/tests/codetoanalyze/java/topl/skip/IndirectSkip.java
@@ -0,0 +1,35 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+import java.util.ArrayList;
+
+class Holder {
+  void doSomething() {}
+}
+
+class MultiHolder {
+  ArrayList<Holder> holders = new ArrayList<>();
+
+  void remove(int i) {
+    Holder h = holders.get(i);
+    h.doSomething();
+    holders.remove(i);
+  }
+
+  int size() {
+    return holders.size();
+  }
+}
+
+class View {
+  MultiHolder mh = new MultiHolder();
+
+  void setCapacityBad(int n) {
+    for (int i = n; i < mh.size(); ++i) {
+      mh.remove(i);
+    }
+  }
+}
diff --git a/infer/tests/codetoanalyze/java/topl/skip/Makefile b/infer/tests/codetoanalyze/java/topl/skip/Makefile
index d168933ce..d53252253 100644
--- a/infer/tests/codetoanalyze/java/topl/skip/Makefile
+++ b/infer/tests/codetoanalyze/java/topl/skip/Makefile
@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../../..
 
-INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 10000 --topl-properties SkipAfterRemove.topl --biabduction-only
+INFER_OPTIONS = --seconds-per-iteration 100 --symops-per-iteration 100000 --topl-properties SkipAfterRemove.topl --biabduction-only
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.java)
diff --git a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
index fb77d5d48..fbc21e954 100644
--- a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
+++ b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
@@ -4,4 +4,4 @@ property SkipAfterRemove
   start -> start: *
   start -> removed: remove(Collection, Index)
   removed -> ok:    get(collection, index)
-  removed -> error: get(collection, J) if j != index
+  removed -> error: get(collection, J) if J != index
diff --git a/infer/tests/codetoanalyze/java/topl/skip/issues.exp b/infer/tests/codetoanalyze/java/topl/skip/issues.exp
index e69de29bb..7fb77e8a0 100644
--- a/infer/tests/codetoanalyze/java/topl/skip/issues.exp
+++ b/infer/tests/codetoanalyze/java/topl/skip/issues.exp
@@ -0,0 +1,2 @@
+codetoanalyze/java/topl/skip/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/skip/IndirectSkip.java, View.setCapacityBad(int):void, 0, TOPL_ERROR, no_bucket, ERROR, []