[Checkers] Arrays and checkers

Matt Papi mpapi at csail.mit.edu
Thu Mar 20 09:48:49 EDT 2008

One more thing: do we have any documentation or test cases for the type 
validator? I couldn't seem to find any.

- Matt

Matt Papi wrote:
> The problem seems to occur because type validator uses fromTypeTree() 
> for array types but getAnnotatedType() on the element of the erased 
> underlying type. fromTypeTree() doesn't add implicit annotations (and it 
> shouldn't) and getAnnotatedType() does (and it should); the interned 
> checker adds an implicit @Interned for the type "Class", so the "use" 
> type is an array of Class but the element type is an array of @Interned 
> class.
> Thinking about the fix raises a design question: we need a way to get 
> the annotated type from a type tree *with* implicit annotations. My 
> proposal: add fromTypeTree(boolean) that calls out to fromTypeTree() and 
> if its parameter is true, calls annotateImplicit(), and use that from 
> the type validator. [I still think having getAnnotatedType() accept type 
> trees is a bad idea, since if checker (!= framework) authors are calling 
> getAnnotatedType() on type trees, they're probably doing something wrong.]
> Also, a side issue: I didn't realize that the type validator issued 
> javac errors. If there's a type floating around that is invalid 
> (according to the type validator), is the cause ever the input program 
> and not a problematic checker? If invalid types are only possible via 
> checker bugs, the validator should probably throw some kind of error or 
> exception instead of issuing a compile error.
> - Matt
> Michael Ernst wrote:
>> Mahmood-
>> I added another failing test case for arrays.
>> There is another failure that I can't seem to reproduce as a small test
>> case.  To reproduce it, see
>>   ~mernst/wisdom/build/build-freepastry
>> and follow the directions.
>> Also, this error message is not comprehensible:
>> /DS/home-0/mernst/tmp/try-freepastry/pastry/src/rice/p2p/util/XMLObjectOutputStream.java:656: invalid type, type need to be a supertype of the required type.
>> found   : java.lang.Class
>> required: @checkers.quals.Interned java.lang.Class
>>     return (Class[]) v.toArray(new Class[0]);
>>                  ^
>> There's an English error ("need" should be "needs"), but more seriously
>> there are 4 uses of "type" in the message, and it's not clear what any of
>> them refer to.
>>                     -Mike
> _______________________________________________
> checkers mailing list
> checkers at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/checkers

More information about the checkers mailing list