[Checkers] NonNull Annotated JDK

[Mahmood Ali]

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