facebook / facebook/infer

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

Open
#2,109 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
OCaml
Stars
15.7k
Forks
2.1k
Avg merge
19h 36m
Merged PRs (30d)
13

Description

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**

```java
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**

```java
import java.io.File;

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

**Reproduction command**

```bash
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.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.