[Checkers] Checking method invocability

[Michael Ernst]

Daniel-

> Well, I actually did not want to check that the arguments are compatible
> but that it is legal to call the method.

The method call is legal exactly if the arguments at the call site are
compatible with the parameters in the method declaration.

> Let say I have to methods
> open() and use() and use() should only occur if open() has been called.
> So as soon as open() is called on an object I need to change the
> object's (to which the methods belong) type and when use() is called I
> do need to check if the type of the object(to which the methods belong)
> is correct.

That sounds right.  I think you really want to know the types of the
parameters and the types of the arguments.  You may be asking for the name
of the method because you thing that will be a good way to get that
information, but the name isn't really want you are after.  Is that
correct?

It would also help me to know what, if anything, of the current checking
framework you are using.  Are you doing your own traversal of the AST, or
just overriding certain methods in the Checker Framework's visitor?

> My problem is now how do I get the type of the object(to
> which the methods belong) within visitMethodInvocation?

A couple terminology clarifications:
 * an expression (such as a variable/reference) has a type; an object has a
   class.
 * methods belong to a type (and implementations belong to a class), not to
   an object.
These distinctions won't matter most of the time, but in technical
conversation it helps to be perfectly clear.

Are you asking for the type of the receiver at the method invocation site?

BaseTypeVisitor.visitMethodInvocation calls two helper methods,
checkMethodInvocability and checkArguments.  These do the same thing, but
for different arguments (the receiver vs. all the others), mostly so that
slightly different error messages can be produced.  The implementations of
these methods seem to do all the checking you need, by comparing the types
on the actual argument and the formal parameter.  You could override this,
but I don't see why you would need to.

Maybe I'm missing something, in which case a more detailed explanation
might clear things up.

> I was thinking about how to annotate a typestate automaton. So the
> return type of the method must not be annotated. Or does the return type
> also reflect the type of the object (to which the method belongs to)?

Perhaps you could propose a syntax, and then we can figure out how to
express it in Java+annotations.  Note that you'll need to express changes
to the types of parameters, not just the receiver.

                    -Mike