[topl] A new test illustrating a false positive

Summary: This comes from github issue #1757

Reviewed By: Gabisampaio

Differential Revision: D45279395

fbshipit-source-id: 805da10fe160871999be58b67d91c8ee11fa97c6

infer/tests/codetoanalyze/java/topl/validRange/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 = --topl-properties validRange.topl --topl-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/topl/validRange/Valid.java

@@ -0,0 +1,23 @@
+/*
+ * 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 Valid {
+  public static boolean is_valid_vn(int i) {
+    return i >= 1 && i <= 10;
+  }
+
+  public static void id_to_vn(int i) {}
+
+  public static void safe_call(int id) {
+    if (is_valid_vn(id)) {
+      id_to_vn(id);
+    }
+  }
+
+  public static void FP_testOk() {
+    safe_call(1);
+  }
+}

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

@@ -0,0 +1 @@
+codetoanalyze/java/topl/validRange/Valid.java, Valid.FP_testOk():void, 0, TOPL_ERROR, no_bucket, ERROR, [call to void Valid.safe_call(int),call to boolean Valid.is_valid_vn(int),call to void Valid.id_to_vn(int)]

infer/tests/codetoanalyze/java/topl/validRange/validRange.topl

@@ -0,0 +1,6 @@
+property ValidVN
+   prefix "Valid"
+   start -> error: "id_to_vn"(IgnoreArg, IgnoreRet)
+   start -> ok: "is_valid_vn"(Arg, Ret) when Ret != 0 => good := Arg
+   ok -> ok: "is_valid_vn"(Arg, Ret) when Ret != 0 => good := Arg
+   ok -> error: "id_to_vn"(Arg, IgnoreRet) when Arg != good