[topl] A test for comparing arguments.

Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.

Reviewed By: ngorogiannis

Differential Revision: D20118863

fbshipit-source-id: b49740d33

infer/tests/codetoanalyze/java/topl/Makefile

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = baos hasnext skip servlet
+SUBDIRS = baos compareArgs hasnext skip servlet
 
 test-%:
 	$(MAKE) -C $* test

infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.java

@@ -0,0 +1,30 @@
+/*
+ * 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.
+ */
+class CompareArgs {
+  static int max(int[] a, int i, int k) {
+    int m = a[i];
+    for (int j = i + 1; j < k; ++j) {
+      m = Math.max(m, a[j]);
+    }
+    return m;
+  }
+
+  static void aBad() {
+    int[] a = new int[10];
+    int x = max(a, 2, 2);
+  }
+
+  static void bOk() {
+    int[] a = new int[10];
+    int x = max(a, 2, 3);
+  }
+
+  static void cBad() {
+    int[] a = new int[10];
+    int x = max(a, 2, 1);
+  }
+}

infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl

@@ -0,0 +1,4 @@
+property MaxArgs
+  nondet (start)
+  start -> start: *
+  start -> error: "CompareArgs.max"(Ignore, I, J, IgnoreRet) when I >= J

infer/tests/codetoanalyze/java/topl/compareArgs/Makefile

@@ -0,0 +1,13 @@
+# 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.
+
+TESTS_DIR = ../../../..
+
+INFER_OPTIONS = --seconds-per-iteration 10 --symops-per-iteration 4000 --topl-properties CompareArgs.topl --biabduction-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/topl/compareArgs/issues.exp

@@ -0,0 +1,2 @@
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
+codetoanalyze/java/topl/compareArgs/CompareArgs.java, CompareArgs.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []