[Checkers] most recent Javari bug

[Mahmood Ali]

Hi Telmo,

I spent some time debugging this problem a bit.

In the case of:
   static <T> void (Map<T, T> map, T key) {
     map.get(key); // currently issue a false positive
   }

The problem is that the parameter is Object.  key's type T defaults   
(T extends @ReadOnly Object), while maps.get parameter is defaults to  
'@Mutable Object'.  Hence the false positive.

Personally, I think that the best solution for you is annotate any  
*use* of Object as ReadOnly by default.  No reference of type 'Object'  
can be used to mutate that object (unless cast is used, or a subclass  
violates subclass rules).

Needless to say, this false positive is eliminated by using the Javari  
annotated JDK.  However, Javari's promise of validity of any un- 
annotated code would be not deliverable.

Regards,
Mahmood

On Aug 10, 2008, at 5:19 AM, Telmo wrote:

> Hello.
>
> I spent the night tracking the bug from the most recent test you  
> committed. A @Mutable annotation is being added to the type of the  
> parameter for the method get, in map. The problem seems to happen  
> because the method is obtained via element, and the mutable  
> annotation is added on the following method in  
> JavariAnnotatedTypeFactory:
>
>    @Override
>    protected void annotateImplicit(Element element, /*\@Mutable*/  
> AnnotatedTypeMirror type) {
>        if (element.getKind().isClass() ||  
> element.getKind().isInterface()) {
>            if (!hasImmutabilityAnnotation(type))
>                type.addAnnotation(MUTABLE);
>        }
>        typePost.visit(type);
>    }
>
> If this method did not override the super method, where would the  
> @ReadOnly annotation from the JDK be received? Just removing the  
> method causes an assertion error, and I will probably be more  
> productive if I have a better idea of where to look.
>
> (That said, I am not sure I will be able to fix this for the next  
> release.)
>
> -Telmo