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

Question

I'm using the checker framework and type annotations to check for correct use of @Nullable and @NonNull. In a Map-like class¹, 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:

• Maven: 3.0.4
• Java: 1.7.0_25 (Oracle)
• Checker framework 1.7.0 (via maven plugin)

This Gist demonstrates the problem.

---

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

Answer 1

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.

Answer 2

When you say

the Java specification states that get(…)-methods return null when the map does not contain an entry for that key

you're right, but only partially right, check here, the javadoc states,

If this map permits null values, then a return value of null does not necessarily indicate that the map contains no mapping for the key; it's also possible that the map explicitly maps the key to null. The containsKey operation may be used to distinguish these two cases.

meaning that, if you're mapping a key to a null value, your method containsKeyStrict could return true and still, your method getStrict would return null, not because there's no value for that key but because that value for that key is precisely null.

To enforce the kind of behavior you need, you could use a HashTable which doesn't allow null values (or keys), or you could add validations to the put methods to prevent the insertion of null values into your map, good luck.