BogusWarning with MonotonicNonNull, RequiresNonNull and super/subtype

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Run the Null Checker on the program below
package test;

import java.util.Set;

import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class Test {
    interface SuperType {
        Set<Runnable> getRunnables();
    }

    static class SubType implements SuperType {
        @MonotonicNonNull
        private Set<Runnable> set;

        @RequiresNonNull("set")
        @Override
        public Set<Runnable> getRunnables() {
            return set;
        }

        void setRunnables(Set<Runnable> newInEdges) {
            assert set == null;
            this.set = newInEdges;
        }
    }
}

What is the expected output? What do you see instead?
Expected: no error
Actual:
@Initialized @NonNull Set<@Initialized @NonNull Runnable> 
getRunnables(@Initialized @NonNull SubType this) in test.Test.SubType cannot 
override 
    @Initialized @NonNull Set<@Initialized @NonNull Runnable> getRunnables(@Initialized @NonNull SuperType this) in test.SuperType; 
    the precondition '@org.checkerframework.checker.nullness.qual.NonNull' for 'this.set' in the subclass method must be weaker (or equally strong) compared to the superclass method

What version of the product are you using? On what operating system?
1.8.6/Windows 8/Java 8

Original issue reported on code.google.com by ClovisSe...@gmail.com on 28 Sep 2014 at 4:36

[GoogleCodeExporter]

This appears to be a valid warning.

The SubType.getRunnables method could be called though a SuperType reference. 
This would bypass the precondition check of @RequiresNonNull("set"), so a 
warning must be issued on the overriding method's declaration. Overriding 
methods must have the same or weaker preconditions than those from the super 
class.

Original comment by mcart...@cs.washington.edu on 19 Nov 2014 at 11:08

• Changed state: Invalid