[Checkers] [Pag] Progress Report

Mahmood Ali mahmood at MIT.EDU
Thu Apr 10 12:44:02 EDT 2008

Hi Mike,

Thank you very much for your comments.

> There is no "@DefaultTypeQualifier" (or some similar name) [...]  
> This differs for NonNull/Interned
> vs. IGJ/Javari.)  Is that on your agenda?
I didn't give this a great thought.  It shouldn't be too difficult to  
do.  However, my initial hunch is that for most checkers (where the  
significant annotation is a subtype annotation, e.g. Interned,  
NonNull, Encrypted, Tained, etc), the default annotation is simply the  
root annotation.

> Also, I notice that the IGJ checker does not use the new meta- 
> annotations,
> nor do other checkers.  Can you fix that, for all the checkers?
All existing checkers except for IGJ and Javari (including  
TestChecker) use the meta-annotations.  I am planning to refactor IGJ  
to take advantage of the meta-annotation.  I would just need to  
override TypeRelations properly to support IGJ relation
	@ReadOnly List<@Mutable Date> <: @ReadOnly List<@ReadOnly Date>

> Finally, can you document these in the manual by the time of the  
> release?
I will try to do that.  I appreciate any help with that!

>> 2. I implemented a test checker that verifies that the
>> factory.getAnnotatedType() returns the appropriate type for the tree.
> Very cool.  I particularly like your implementation approach -- you  
> write a
> Checker that does all the work.  That is a very nice way to package  
> up the
> functionality.  (And it isn't what I would have thought of first.)
I am glad that you liked it!

The downside of this is that the annotated type factory should always  
return fully annotated type and never get further enriched in the  

I have another testing proposal for testing isSubtype() that I will  
detail in a later email.  I am not planning to work on this for  
another week or two!

>> the Javari factory returns types containing multiple annotations  
>> '@Mutable
>> @ReadOnly JavariCell' which violates the TypesRelations check.
> This sounds like a bug in the Javari checker.  Is that correct?
Correction: typo correction: @Mutable @RoMaybe JavariCell not @Mutable  
@ReadOnly JavariCell

It is not quite a bug since the framework has no specification yet  
regarding how types are annotated.

There are many implicit assumptions on how the framework words (like  
the one above).  We should document them in the manual.

  -M ahmood

More information about the checkers mailing list