facebook / facebook/infer

[Question] Are heuristics used when calculating the preconditions of functions?

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

Description

```
import java.lang.IllegalArgumentException;

class Obj {
Object x;

public Object getX() {
return null;
}
}

public class Main {
public int g(int j) {
if (j >= 10) {
return j + 1;
}
else if (j >= 5) {
return j;
}
else {
return 0;
}
}

public int f(int i) {
int j = g(i + 1);

if (j == 0) {
throw new IllegalArgumentException();
}
else if (j == 6) {
return j;
}

Obj obj = new Obj();

Object x = obj.getX();
String str = x.toString(); // NPE
return str.length();
}
}
```
I analyzed this Java program using Infer's Pulse module.
While Pulse did not catch the NPE directly, I confirmed that it did detect the error as a latent issue.
During this process, I checked whether the precondition for function `f` was calculated correctly.
I found that the precondition related to the variable `i` in `f` was empty.
Because of this, I was wondering if there might be a heuristic that ignores the return value of functions that simply return a constant.
If I have misunderstood the relationship, I would appreciate it if you could let me know.

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.