FALSE NEGATIVE: BUFFER_OVERRUN_L1 misses a fixed array overrun after an ArrayList join

[lynae99]

Hi, I found a false negative in Infer 1.3.0 when an empty local ArrayList is joined with an ArrayList returned by an interface method before an enhanced-for loop.

Affected tool

Infer 1.3.0

Affected checker

Infer BUFFER_OVERRUN_L1

Minimal reproducer

import java.util.ArrayList;

class InferBufferOverrunArrayListJoin {
  interface Factory { ArrayList<Integer> make(); }

  void test(Factory factory, boolean chooseEmpty) {
    ArrayList<Integer> values = chooseEmpty ? new ArrayList<>() : factory.make();
    for (Integer value : values) {
      int[] data = new int[1];
      data[1] = value;
    }
  }
}

Reproduction command

infer --version
infer run --bufferoverrun --enable-issue-type BUFFER_OVERRUN_L1 -- javac spotbugs-to-infer-buffer-overrun-fn-arraylist-join.java

Current behavior

Infer completes successfully but produces no BUFFER_OVERRUN_L1 diagnostic. The equivalent loop over factory.make() directly is reported, as is a join between the empty list and an ArrayList parameter.

Expected behavior

Infer should report data[1] because when chooseEmpty is false and factory.make() returns a nonempty list, the loop executes and index 1 is outside the length-1 array.