[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

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

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)

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

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, []