[Checkers] NonNull Annotated JDK

Matt Papi mpapi at csail.mit.edu
Sun Apr 6 15:03:26 EDT 2008


Thanks for pointing that out. I haven't been updating the @Default
mechanism with respect to recent framework changes (like
annotateInheritedFromClass()). If that's really the cause, the fix
should be pretty easy -- I'll see if I can have it in soon.

- Matt

On Sun, Apr 6, 2008 at 2:57 PM, Mahmood Ali <mahmood at mit.edu> wrote:
>  On Apr 6, 2008, at 2:43 PM, Mahmood Ali wrote:
>  > 2. Prepare the Annotated (method signitures only) JDK for Matt.  It is
>  > available now on ~mali/research/jdk/nonnull.  Unfortunately, it
>  > doesn't type check currently under the nonnull checker.  I suspect
>  > that the bug is in TypesRelations, but I will need to investigate it
>  > more later.  The issued warnings are all due to override related issue
>  > (66 for receiver incompatible type!).
>  I take my suspicion back.  After a closer examination of the output
>  messages, I notice that that a lot of them are due to the default
>  annotation (@NonNull) showing up in the type arguments.  There errors
>  are in the form:
>  AbstractCollection.java:6: iterator() in java.util.AbstractCollection
>  cannot override iterator() in java.util.Collection; attempting to use
>  an incompatible return type
>  found   : @NonNull @checkers.quals.Default("checkers.quals.NonNull")
>  java.util.Iterator<E extends @NonNull java.lang.Object>
>  required: @checkers.quals.Default("checkers.quals.NonNull")
>  java.util.Iterator<E extends java.lang.Object>
>    public abstract java.util.Iterator<E> iterator();
>  Also, the default annotates the method receiver with @NonNull, so the
>  overrider method has more strict receiver type as the overriden method
>  is not annotated with @NonNull.  These errors are in the form (Please
>  note that the type arguments don't matter here, as we only test the
>  erased receiver type):
>  AbstractCollection.java:7: size() in java.util.AbstractCollection
>  cannot override size() in java.util.Collection; attempting to use an
>  incompatible receiver type
>  found   : @NonNull java.util.AbstractCollection<E extends @NonNull
>  java.lang.Object>
>  required: java.util.Collection<E extends java.lang.Object>
>    public abstract int size();
>                        ^
>  Sometimes the default annotations isn't actually added properly.
>  That's the case of:
>  AbstractCollection.java:16: removeAll(java.util.Collection<?>) in
>  java.util.AbstractCollection cannot override
>  removeAll(java.util.Collection<?>) in java.util.Collection; attempting
>  to use an incompatible parameter type
>  found   : @NonNull @checkers.quals.Default("checkers.quals.NonNull")
>  java.util.Collection<?>
>  required: @checkers.quals.Default("checkers.quals.NonNull")
>  java.util.Collection<?>
>    public boolean removeAll(java.util.Collection<?> a1) { throw new
>  RuntimeException("skeleton method"); }
>  I haven't checked every single error, but they all look as variations
>  of the previous three error messages.
>  Regards,
>  Mahmood
>  _______________________________________________
>  checkers mailing list
>  checkers at lists.csail.mit.edu
>  https://lists.csail.mit.edu/mailman/listinfo/checkers

More information about the checkers mailing list