Fails to Catch Simple Interprocedural Java NPE

[matjin]

In the following simple piece of code:

https://gist.github.com/matjin/0499c1c00c44394a4abbb21d50536aff

Infer is unable to find the null dereference warning at line 18; interprocedural analysis is not executed. There is a warning at line 28, though, as you can see below. If bar() is commented out, Infer says there are no issues.

Infer's report on the example is as follows, for the following command:

infer run --debug -- javac App.java

---

Found 2 issues

App.java:28: warning: ANALYSIS_STOPS (biabduction/Rearrange.ml:1623:55-62:) exception: NULL_DEREFERENCE. 26.

27. x.b = true;

28.     int y = x.MayReturnNull().f;

30. x.b = false;

App.java:28: error: NULL_DEREFERENCE (biabduction/Rearrange.ml:1623:55-62:) [B1] object returned by x.MayReturnNull() could be null and is dereferenced at line 28. 26.

27. x.b = true;

28.     int y = x.MayReturnNull().f;

30. x.b = false;

Summary of the reports

ANALYSIS_STOPS: 1

NULL_DEREFERENCE: 1

---

Version/platform information: Infer version v0.16.0-2a0ec8c0d

Operating System: Ubuntu 18.04.2 LTS Kernel: Linux 4.18.0-1014-azure Architecture: x86-64

[SolomonSun2010]

add --pulse option could help you.

[SolomonSun2010]

MyBar1A.java use your Foo1A.java as below， Infer cannot report the NPE too !

/**
 * infer --debug --pulse -- javac MyBar1A.java
 */
public class MyBar1A {

    public static void main (String[] args) {
        String value = provide();
        consume(value);
    }

    public static String provide() {
        return Foo1A.provide(); // use Foo1A
    }

    public static void consume(String value) {
        String value2 = value.toLowerCase(); // ERROR
        System.out.println(value2);
    }
}