EnsuresNonNull failing on generic method parameters

[Johannes-Rost]

Hello,

I have come across an issue while using @EnsuresNonNull on method parameters with certain generic types.

If I have the following method

public class CollectionContracts {

    @EnsuresNonNull("#1")
    public static <T extends Collection<E>, E> @NonNull T requireNotEmpty(T collection) {
        if(collection == null) {
            throw new IllegalArgumentException("Collection was null");
        }
        if(collection.isEmpty()) {
            throw new IllegalArgumentException("Collection was empty");
        }
        return collection;
    }
}

the compilation fails with the following error message:

[...]/CollectionContracts.java:4:59
java: [contracts.postcondition] postcondition of requireNotEmpty is not satisfied.
  found   : no information about collection
  required: collection is @NonNull

If I change the signature to

    @EnsuresNonNull("#1")
    public static <E> @NonNull Collection<E> requireNotEmpty(Collection<E> collection) {

everything work as I would expect.

I am using checker-framework version 3.42.0 with maven-compiler-plugin 3.12.1

[Johannes-Rost]

You can find the example under https://github.com/WPS/common-contracts/blob/main/src/main/java/de/wps/common/contracts/CollectionContracts.java

[Johannes-Rost]

If I add an @nullable to the first argument, everthing works as expected:

public class CollectionContracts {

    @EnsuresNonNull("#1")
    public static <T extends Collection<E>, E> @NonNull T requireNotEmpty(@Nullable T collection) {
        if(collection == null) {
            throw new IllegalArgumentException("Collection was null");
        }
        if(collection.isEmpty()) {
            throw new IllegalArgumentException("Collection was empty");
        }
        return collection;
    }
}

What I still do not know is, why there is a difference between my two examples in the first post...

[mernst]

Thanks for letting us know the workaround. I would like @smillst to take a quick look regardless, so I'm re-opening this.