FALSE NEGATIVE: Pulse misses a possible null dereference from `BufferedReader.readLine()`

[chisa22]

Hi, I found a false negative in Infer 1.3.0 when BufferedReader.readLine() may return null at end of input.

Affected tool

Infer 1.3.0

Affected checker

Infer NULLPTR_DEREFERENCE

Minimal reproducer

import java.io.BufferedReader;
import java.io.IOException;

class InferNullReadLine {
  int test(BufferedReader reader) throws IOException {
    String line = reader.readLine();
    return line.length();
  }
}

Additional reproducer

import java.io.File;

class InferNullFileList {
  int test(File file) {
    File[] files = file.listFiles();
    return files.length;
  }
}

Reproduction command

infer --version
infer run --pulse --bufferoverrun --enable-issue-type NULLPTR_DEREFERENCE -- javac spotbugs-to-infer-nullptr-fn-readline.java

Current behavior

Infer completes successfully but produces no NULLPTR_DEREFERENCE finding for either BufferedReader.readLine() or File.listFiles().

Expected behavior

BufferedReader.readLine() may return null at end of input, so Pulse should report the dereference in the minimal reproducer.

File.listFiles() is documented to return null when the path does not denote a directory or when an I/O error occurs. Pulse should model this nullable return value so that dereferencing the result without a null check can be reported.