java-8non-nullablejava-annotationschecker-framework

Multiple @EnsuresNonNullIf should be ok; but the compiler complains


The manual of the Checker Framework claims "You can write multiple @EnsuresNonNullIf annotations on a single method", however I observe the following message if I try this:

@EnsuresNonNullIf(expression="getFieldNames()", result=true)
@EnsuresNonNullIf(expression="getFieldName(i)", result=true)
public boolean hasFieldNames() {
    return fFieldNames != null;
}

The resulting error message by the Eclipse Java compiler:

Duplicate annotation of non-repeatable type @EnsuresNonNullIf. Only annotation types marked @Repeatable can be used multiple times at one target.

The resulting error message by the MVN javac compiler:

[ERROR] Blabla.java:[?,?] org.checkerframework.checker.nullness.qual.EnsuresNonNullIf is not a repeatable annotation type

I'm annotating 10-year-old code, so I'm hoping some configuration trick can safe the day :-) Without the multiple @EnsuresNonNullIf I'm up for quite a bit of manual code annotation to fix false positives that I'm not interested in...

PS: I tried using both checker-framework-2.8.1 and 2.9.0 with similar results, and always using <maven.compiler.source>1.8</maven.compiler.source>


Solution

  • I found this issue on the Checker Framework issue tracker: https://github.com/typetools/checker-framework/issues/1307

    It explains an "enhancement" request for adding @Repeatable to the following CF annotations:

    >  @DefaultQualifier -- DONE
    >  @EnsuresKeyFor
    >  @EnsuresKeyForIf
    >  @EnsuresLockHeldIf
    >  @EnsuresLTLengthOf
    >  @EnsuresLTLengthOfIf
    >  @EnsuresMinLenIf
    >  @EnsuresNonNullIf
    >  @EnsuresQualifier -- DONE
    >  @EnsuresQualifierIf -- DONE
    >  @FieldInvariant
    >  @GuardSatisfied
    >  @HasSubsequence
    >  @MethodVal
    >  @MinLenFieldInvariant
    >  @RequiresQualifier -- DONE
    >  @SubstringIndexFor
    

    And the discussion contains a workaround, since EnsuresQualifiersIf is already repeatable:

    @EnsuresQualifiersIf({
        @EnsuresQualifierIf(result=true, qualifier=NonNull.class, expression="getFoo()"),
        @EnsuresQualifierIf(result=false, qualifier=NonNull.class, expression="getBar()")
    })
    boolean hasFoo();
    

    And in my case that works out to:

     @EnsuresQualifiersIf({
        @EnsuresQualifierIf(result=true, qualifier=NonNull.class, expression="getFieldNames()"),
        @EnsuresQualifierIf(result=true, qualifier=NonNull.class, expression="getFieldName(i)")
    })
    public boolean hasFieldNames() {
        return fFieldNames != null;
    }