javaannotationschecker-frameworktype-annotation

@EnsuresNonNullIf annotation gives "conditional postcondition not satisfied"-warning

I'm using the checker framework and type annotations to check for correct use of @Nullable and @NonNull. In a Map-like class1, the Java specification states that get(…)-methods return null when the map does not contain an entry for that key. Therefore, the methods have the @Nullable-annotation. However, when contains(…) returns true, I like to guarantee that get(…) will not return null.

How can I do specify conditional NonNull?

As far as I know, you can achieve this by annotating the contains(…)-methods with @EnsuresNonNullIf, as follows:

@Pure
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true)
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) {
    return super.containsKey(key);
}

@Pure
public @Nullable TValue getStrict(final @Nullable Class<? extends TKeyClass> key) {
    Return super. gets (key);
}

However, this causes a warning:

the conditional postcondition about 'this.getStrict(key)' at this return statement is not satisfied

How should I solve this "postcondition not satisfied"-warning?

My environment:

This Gist demonstrates the problem.

1) It extends map's functionallity with to retrieve entries with "similar" keys.

Solution

  • Up to now, my only solution is to combine the @EnsuresNonNullIf-annotation with SuppersWarnings("nullness"). E.g.:

    @SuppressWarnings("nullness")
@EnsuresNonNullIf(expression = {"get(#1)", "getMatchingStoredKey(#1)", "getStrict(#1)", "lookup(#1)"}, result = true)
public boolean containsKeyStrict(final @Nullable Class<? extends TKeyClass> key) {
    return super.containsKey(key);
}

    To scope the @SuppressWarnings you can delegate the implementation to a method not annotated @EnsuresNonNullIf.