[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