typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
990 stars 347 forks source link

Support for javax.annotation.Nonnegative annotation #6507

Closed Lmh-java closed 2 months ago

Lmh-java commented 2 months ago

Hi, I am a contributor to Checkstyle. I am working on resolving the violation attached below.

<checkerFrameworkError unstable="false">
    <fileName>src/main/java/com/puppycrawl/tools/checkstyle/DetailAstImpl.java</fileName>
    <specifier>argument</specifier>
    <message>incompatible argument for parameter arg0 of BitSet.get.</message>
    <lineContent>return getBranchTokenTypes().get(tokenType);</lineContent>
    <details>
      found   : int
      required: @NonNegative int
    </details>
  </checkerFrameworkError>

Relevant code:

@Override
public boolean branchContains(@NonNegative int tokenType) {
    return getBranchTokenTypes().get(tokenType);
}

However, it seems that checker-framework does not support the @Nonnegative annotation from javax.annotation. (I guess it is because JSR 305 is abandoned?) When I was trying to use @Nonnegative(from Javax) to replace @NonNegative (from Checker Framework), the above error would still be given. In our case, it would be nice if we just original Java annotation instead of introducing a new one.

I just want to confirm whether it is true that checker-framework only supports 3 annotations from Javax (as stated here https://checkerframework.org/releases/2.3.1/api/index.html?javax/annotation/package-summary.html), excluding @Nonnegative. Do you have some recommendations for solving this problem? Thank you very much!

kelloggm commented 2 months ago

I can confirm that we currently don't treat these two annotations the same. You're right that we haven't added support for this kind of aliasing because JSR 305 is abandoned, but also we haven't done so because no one has asked about it, until now :)

I opened a PR (#6508) to add support for the alias - it's pretty straightforward on our end. Hopefully it will appear in the next Checker Framework release.

Lmh-java commented 2 months ago

Thanks a lot for your reply and pull request. I truly appreciate that. :) 👍