[inferbo] Fix check of access condition

Reviewed By: mbouaziz

Differential Revision: D13114160

fbshipit-source-id: 9e46cf814

Makefile

@@ -107,8 +107,22 @@ BUILD_SYSTEMS_TESTS += \
 	racerd_dedup
 
 DIRECT_TESTS += \
-  java_checkers java_classloads java_eradicate java_infer java_lab java_tracing java_quandary \
+  java_checkers \
-  java_racerd java_stability java_crashcontext java_hoisting java_hoistingExpensive java_starvation java_performance java_purity
+  java_classloads \
+  java_crashcontext \
+  java_eradicate \
+  java_hoisting \
+  java_hoistingExpensive \
+  java_infer \
+  java_lab \
+  java_performance \
+  java_purity \
+  java_quandary \
+  java_racerd \
+  java_stability \
+  java_starvation \
+  java_tracing \
+
 ifneq ($(ANT),no)
 BUILD_SYSTEMS_TESTS += ant
 endif

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -260,7 +260,8 @@ module ArrayAccessCondition = struct
        For adding into collections : we want to check that 0 <= idx <= size *)
     let real_idx = ItvPure.plus c.offset c.idx in
     let size =
-      ItvPure.make_positive (if c.is_collection_add then ItvPure.succ c.size else c.size)
+      let size_pos = ItvPure.make_positive c.size in
+      if c.is_collection_add then ItvPure.succ size_pos else size_pos
     in
     (* if sl < 0, use sl' = 0 *)
     let not_overrun =

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -0,0 +1,28 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+package codetoanalyze.java.bufferoverrun;
+
+import java.util.ArrayList;
+
+class Array {
+  private ArrayList a = new ArrayList<>();
+
+  void collection_add_zero_Good() {
+    a.add(0, 100);
+  }
+
+  ArrayList collection_add_zero_Bad() {
+    ArrayList b = new ArrayList<>();
+    b.remove(0);
+    return b;
+  }
+
+  void collection_add_zero2_Good() {
+    ArrayList b = collection_add_zero_Bad();
+    b.add(0, 100);
+  }
+}

infer/tests/codetoanalyze/java/bufferoverrun/Makefile

@@ -0,0 +1,15 @@
+# Copyright (c) 2018-present, Facebook, Inc.
+#
+# 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 = --bufferoverrun-only --no-filtering --debug-exceptions \
+                --project-root $(TESTS_DIR)
+
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/bufferoverrun/issues.exp

@@ -0,0 +1 @@
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_add_zero_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 0 Size: 0]