[Checkers] Receiver and result annotations for constructors

[Michael Ernst]

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