[Checkers] Receiver and result annotations for constructors
Michael Ernst
mernst at csail.mit.edu
Thu Jun 5 06:26:28 EDT 2008
Telmo-
> I wasn't aware of the possibility of adding annotations between new
> and the new class name.
>
> What annotations should be added to the new object, though? Namely, if one
> writes
>
> new @A SomeObject();
>
> and the constructor of SomeObject takes the form
>
> SomeObject() @B { ... }
>
> should the created type have both the @A and @B annotations?
No, just @A. The @B annotation is on the *receiver*, not the result.
In particular, for a non-inner class, that annotation is illegal.
For an inner class, @B is a requirement on one of the parameters -- the
receiver (which is of the outer class). Analogously, in this code
SomeObject(@C Object) @B { ... }
@C is a requirement on a different parameter to the constructor.
Now, if you had written
myvar = new @A SomeObject();
@D SomeObject() { ... } // new syntax I hadn't considered until just now
then the type of myvar is annotated with both @A and @D. We can discuss
whether the framework should take care of this.
-Mike
More information about the checkers
mailing list