[Checkers] [Pag] Progress Report

Michael Ernst mernst at csail.mit.edu
Thu Apr 10 08:34:39 EDT 2008


Mahmood-

Thanks for your detailed progress report, and for all the good progress you
have made over the past week.  (And forgive me for replying to the entire
checkers mailing list, but I think many of the issues will be of interest
to them.)

> I added multiple meta-
> annotations (e.g. @TypeQualifier, @RootTypeQualifier, @SubtypeOf({ })  
> @TypeQualifiers({ })) that are used by BaseTypeChecker to build the  
> annotation hierarchy. This enables one to simply specify declare the  
> type qualifiers need to be checked, and then the framework infer all  
> the relationships and enforce the necessary checks.

There is no "@DefaultTypeQualifier" (or some similar name) annotation to
indicate which annotation should be assumed if the programmer has not
written any annotation.  (This differs for NonNull/Interned
vs. IGJ/Javari.)  Is that on your agenda?

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?  (This is
somewhat related to your point #5 about refactoring the IGJ factory to take
better advantage of the framework.)

Finally, can you document these in the manual by the time of the release?

> 2. I implemented a test checker that verifies that the  
> factory.getAnnotatedType() returns the appropriate type for the tree.   
> One simply need to specify the expected type in comment either in the  
> same line or the previous line.  Something like:
> 	List<@NonNull String> l = Collections.emptyList();  ///  
> Collections.emptyList() -:- List<@NonNull String>

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.)

> 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?

                    -Mike



More information about the checkers mailing list