[Checkers] @ReadOnly classes

Mahmood Ali mahmood at MIT.EDU
Tue Mar 25 23:40:31 EDT 2008

Hi Telmo,

> as of now,
> @ReadOnly class ReadOnlyEmpty {}
> generates an error, (receiver.invalid), because not every method on  
> Object
> has a @ReadOnly receiver.

The error you are getting is actually due a different issue.  The Sun  
Javac compiler automatically add a constructor tree whose receiver is  

In JavariVisitor.visitMethod(), you check whether you have a mutable  
method within a readonly class without checking that the method is a  

I assume that the solution is that you allow to have mutable  
constructors within a readonly class, i.e. check method receivers only  
for non-constructors. Please note TreeUtils.isConstructor().

I will try to comment on the rest of your email later.

- Mahmood

More information about the checkers mailing list