FALSE NEGATIVE: Pulse misses a possible null dereference from `BufferedReader.readLine()`
- 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
Assessment
This issue has not been assessed yet.