Anonymous inner class and @MonotonicNonNull

[GoogleCodeExporter]

Not sure if this is a bug or a misunderstanding on my part, but I think I'm 
getting a false positive.  Using Checker Framework v1.7.1 on Java 1.7.0_25, on 
Mac OS X 10.8.5.

    /*>>> import checkers.nullness.quals.MonotonicNonNull; */

    abstract class Monotonic
    {
        public /*@MonotonicNonNull*/String header;

        public void f()
        {
            if (header == null) {
                write("null");
            }
            else {
                runWithRetry(new Runnable() {
                    public void run() {
                        write(header);  // <-- error here
                    }
                });
            }
        }

        public abstract void write(String s);
        public abstract void runWithRetry(Runnable r);
    }

I expected no errors, but I got one:

# java -jar binary/checkers.jar -processor checkers.nullness.NullnessChecker 
Monotonic.java
Monotonic.java:15: error: incompatible types in argument.
                    write(header);
                          ^
  found   : @Initialized @MonotonicNonNull String
  required: @Initialized @NonNull String
1 error

If I replace the runWithRetry and the anonymous inner class with a simple 
"write(header)", there are no errors.

Original issue reported on code.google.com by kan...@cakoose.com on 18 Dec 2013 at 1:39

[GoogleCodeExporter]

Hi Kannan,
thanks for this report!
This is an unfortunate limitation of our current flow framework. See the last 
comment in Issue 266: 
https://code.google.com/p/checker-framework/issues/detail?id=266
The work-around suggested there is to introduce a final local variable.
Would such a work-around be impractical?
We should definitely add a note to the manual/faq about this.

Original comment by wdi...@gmail.com on 18 Dec 2013 at 2:17

• Changed state: Accepted

[GoogleCodeExporter]

The local variable workaround is good enough for my case.

Documenting this limitation would be nice, but it seems hard for a user like me 
to find the relevant docs.  Is it feasible to notice when the extra information 
is being thrown away and mention this fact in the error message?  Maybe 
something like "some type information was lost, see https://blah/blah for more 
information".

Original comment by kan...@cakoose.com on 18 Dec 2013 at 2:34

[mernst]

This is still a problem in Checker Framework version 2.3.2.