diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/Makefile b/infer/tests/codetoanalyze/java/topl/slowIter/Makefile new file mode 100644 index 000000000..b36e06160 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/slowIter/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 20000 --topl-properties slowIter.topl --biabduction-only +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.java) + +include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java new file mode 100644 index 000000000..465566a22 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/slowIter/SlowIterTests.java @@ -0,0 +1,34 @@ +/* + * 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.Map; + +class SlowIterTests { + // T62611635 + static void FN_aBad(Map m) { + for (K k : m.keySet()) { + System.out.printf("%s -> %s\n", k, m.get(k)); + } + } + + static void aOk(Map m) { + for (Map.Entry e : m.entrySet()) { + System.out.printf("%s -> %s\n", e.getKey(), e.getValue()); + } + } + + // Inter-procedural variant of aBad. + static void FN_bBad(Map m) { + for (K k : m.keySet()) { + print(k, m); + } + } + + static void print(K k, Map m) { + System.out.printf("%s -> %s\n", k, m.get(k)); + } +} diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl new file mode 100644 index 000000000..54500efe0 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl @@ -0,0 +1,8 @@ +property ShouldUseEntries + nondet (start iteratingKeys) + start -> start: * + start -> gotKeys: S = "Map.keySet"(M) + gotKeys -> iteratingKeys: I = "Set.iterator"(s) + iteratingKeys -> iteratingKeys: * + iteratingKeys -> gotOneKey: K = "Iterator.next"(i) + gotOneKey -> error: ".*Map.get"(m, k)