@EnsuresNonNullIf doesn't seem to work as expected when used in a superclass

[diegovar]

Here's a live example:

http://eisop.uwaterloo.ca/live#mode=display&code=import+org.checkerframework.checker.nullness.qual.Nullable%3B%0Aimport+org.checkerframework.checker.nullness.qual.EnsuresNonNullIf%3B%0Aimport+org.checkerframework.dataflow.qual.Pure%3B%0A%0Aabstract+class+Animal+%7B%0A++%40Pure%0A++%40EnsuresNonNullIf(expression%3D%22asDog()%22,+result%3Dtrue)%0A++boolean+isDog()+%7B%0A++++return+false%3B%0A++%7D%0A++%0A++%40Nullable%0A++Dog+asDog()+%7B%0A++++return+null%3B%0A++%7D%0A%7D%0A%0Aclass+Dog+extends+Animal+%7B%0A++++%40Override%0A++++boolean+isDog()+%7B%0A++++++++return+true%3B%0A++++%7D%0A++++%0A++++%40Override%0A++++Dog+asDog()+%7B%0A++++++++return+this%3B%0A++++%7D%0A%7D&typeSystem=nullness

As you can see, this fails to validate and I'm unsure why.

[mernst]

The answer is in the error message:

Conditional postcondition must be no weaker than in superclass.

The superclass has an @EnsuresNonNullf annotation, so the subclass needs one too.
You didn't write one on the subclass, and the error message is telling you that you need to.

[wmdietl]

@EnsuresNonNullIf is annotated with @InheritedAnnotation: https://github.com/typetools/checker-framework/blob/master/checker/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java#L80

I would not expect that the subclass would need to repeat the @EnsuresNonNullIf.
The second error about the implementation also only makes sense if the @EnsuresNonNullIf is inherited, otherwise there is no contract that could be violated.

[wmdietl]

One possible cause is that the expression gets substituted incorrectly, using super instead of this.

[smillst]

For pre/post conditions, this.methodCall() and super.methodCall() should be equivalent.

[smillst]

The contracts both parse to this.asDog(), but the MethodCall objects for asDog have different method elements, so the two FlowExpressions are not equal.

[smillst]

Here's another example of problems with contracts with overriden methods.

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

public class Simple {
    static class Super {
        @Nullable String name() {
            return "";
        }

        @RequiresNonNull("name()")
        void requiresNonNull() {
            name().equals("");
        }
    }

    static class Sub extends Super {
        @Override
        @Nullable String name() {
            return null;
        }

        void method() {
            if (super.name() != null) {
                // This error is correctly issued.
                // :: error: contracts.precondition.not.satisfied
                super.requiresNonNull(); 
            }
            if (this.name() != null) {
                // This error is issued, but shouldn't be.
                // :: error: contracts.precondition.not.satisfied
                super.requiresNonNull(); 
            }
        }
    }

    public static void main(String[] args) {
        new Sub().method();
    }
}

More test cases with various false positives and false negatives:
https://github.com/typetools/checker-framework/blob/ebb6add20d448b017cd79b2b8413fa509853df1f/checker/tests/nullness/Issue2013.java.

[negora]

I'm getting a similar error when creating an interface and a class that implements it:

public final class Example {

	private static interface Record {

		@Pure
		public @Nullable Integer getId ();

		@Pure
		@EnsuresNonNullIf (result = true, expression = "getId ()")
		public boolean hasId ();

	}


	private static final class MutableRecord
			implements Record {

		private @Nullable Integer id;

		public MutableRecord () {
		}

		@Override
		public @Nullable Integer getId () {
			return id;
		}

		public void setId (@Nullable Integer id) {
			this.id = id;
		}

		@Override
		public boolean hasId () {
			return getId () != null;
		}

	}

}

As a workaround, I've had to convert hasId () into a static method, and implement it directly in the interface:

		@Pure
		@EnsuresNonNullIf (result = true, expression = "#1.getId ()")
		public static boolean hasId (Record record) {
			return record.getId () != null;
		}

Then I've been able to call it this way:

MutableRecord record = new MutableRecord ();
// More code...
if (Record.hasId (record)) {
  Integer id = record.getId ();
}

But, obviously, it looks like a little unnatural.

Edit: using a default method in the interface seems to be another workaround too. But, again, you can't override such method in the concrete class without getting an error from Checker Framework.

[DavyLandman]

We just ran into the same problem, is there a workaround?

[ERROR] C:\Users\Davy\swat.engineering\rascal\vallang\src\main\java\io\usethesource\vallang\impl\fields\AbstractDefaultWithKeywordParameters.java:[95,19] error: [contracts.conditional.postcondition.true.override] Subclass postcondition with result=true is weaker for 'this.getParameter(label)' in hasParameter.
[ERROR]     In superclass io.usethesource.vallang.IWithKeywordParameters: @NonNull
[ERROR]
[ERROR]     In subclass io.usethesource.vallang.impl.fields.AbstractDefaultWithKeywordParameters: no information

with:

public interface IWithKeywordParameters<T extends IValue> {

    public <X extends @Nullable IValue> X getParameter(String label);

    @EnsuresNonNullIf(expression="getParameter(#1)", result=true)
    public boolean hasParameter(String label);
...

and a down subclass

public abstract class AbstractDefaultWithKeywordParameters<T extends IValue> implements IWithKeywordParameters<T> {

...

    @SuppressWarnings("unchecked")
    @Override
    public <X extends @Nullable IValue> X getParameter(String label) {
        return (X) parameters.get(label);
    }

    @Override
    @EnsuresNonNullIf(expression="getParameter(#1)", result=true)
    public boolean hasParameter(String label) {
        return parameters.containsKey(label);
    }