Nullness Checker: method framing mistake

The attached file checks without warning with the Nullness Checker, yet 
produces an NPE at runtime:

$ ./bin-devel/javac -processor 
org.checkerframework.checker.nullness.NullnessChecker Issue425.java 

$ java Issue425
Exception in thread "main" java.lang.NullPointerException
    at Issue425.fail(Issue425.java:22)
    at Issue425.main(Issue425.java:27)

Tested with both 1.8.11 and trunk as of today (2015-04-04).

The cause might be that these two features are not handled in the correct order:
- after a method call, the receiver can be assumed to be non-null.
- after a non-pure method call, fields might have changed.

Dealing with this soundly might result in many more errors and we need to think 
of a good way to add better framing.

Original issue reported on code.google.com by wdi...@gmail.com on 4 Apr 2015 at 2:52

Attachments:

• Issue425.java

Start with the attached Issue425.java and reproduce the reported commands using the NullnessChecker, then compare the checker result with the runtime NPE at Issue425.fail. Investigate the ordering of receiver non-null assumptions and non-pure method field changes; done means the unsound behavior is addressed without introducing an unreviewed framing design.