[Checkers] Fwd: Universe Type System Checker

Mahmood Ali mahmood at MIT.EDU
Tue Dec 2 17:57:04 EST 2008



Begin forwarded message:

> From: Phokham Nonava <poky at student.ethz.ch>
> Date: December 1, 2008 12:05:47 PM EST
> To: Mahmood Ali <mahmood at MIT.EDU>
> Cc: "Werner M. Dietl" <Werner.Dietl at inf.ethz.ch>
> Subject: Universe Type System Checker
>
> Greetings Mahmood,
>
> We've been using the checker framework now for quiet a while and our  
> Universe Type System checker finally makes some progress. We  
> struggled about some issues with the framework though. Maybe you can  
> clear things up a little bit. Attached to this mail you'll find an  
> alpha version of our checker. Here are our problems:
>
> * Problem with generic inner classes
>
> Have a look at test/uts/GenericClasses.java. We have a problem that  
> the @Peer annotation from "new @Peer ListInner<@Rep Data>()" on line  
> 41 was not available. On the generic outer class it shows up just  
> fine.
>
> To show the issue just uncomment testGenericClasses() in tests/src/ 
> tests/UtsTest.java and visitVariable() in src/checker/uts/ 
> UtsVisitor.java. You'll see if you execute UtsTest.java that the  
> generic inner class is missing the @Peer annotation.
>
> * Problems executing the tests with version 0.8.2 on Windows
>
> I couldn't manage to run more than 1 test case with the framework  
> version 0.8.1 and 0.8.2. For example in BasicTest.java only  
> testSimple() executed fine. testPoly() aborted with an error. If I  
> commented out testSimple(), testPoly() would run just fine. Maybe  
> you can give me a hint. There are no problems with version 0.8.0.
>
> * isValidUse() and return types of methods
>
> On line 65 of the test file tests/uts/Basic.java we have a method
>
> private @Any @Rep Object testWFTypeReturn()
>
> In isValidUse() we wanted to check for types with multiple  
> annotations. It seems that isValidUse() will not be called on the  
> return type of testWFTypeReturn(). So we had to make the return type  
> check separately with visitMethod() in UtsVisitor.java. Is this by  
> design or do we made a mistake?
>
> We would be happy if you could clear things up for us :). Thanks a  
> lot!
>
> Best regards,
> Phokham
-------------- next part --------------
A non-text attachment was scrubbed...
Name: checkers.zip
Type: application/zip
Size: 26296 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20081202/35aa5781/attachment-0001.zip 
-------------- next part --------------



More information about the checkers mailing list