[Checkers] Framework changes

[Michael Ernst]

Mahmood-

> Mike has proposed a solution regarding adding default annotations to a  
> type. Currently, each checker is implementing it in his own checker. I  
> will coordinate with Matt to implement it.

This coordination is a good idea.  We don't want to waste any time on
duplicated work, and when two people's work conflicts, that's even worse.

I've suggested that Matt create a text file of to-do items.  It's less
featureful than a bug database, but probably adequate for our needs.  We
can use this to claim tasks (by adding a name to a task), so as to avoid
conflicts.

Another thing that would be good is design reviews.  If you find a problem,
please propose a solution for others to review.  The above is another good
example.  You noticed a problem that others had overlooked before, which
was great.  But the proposed fixes were bad for one checker or another, and
only after discussion did we come up with the clean, general solution of
inheriting annotations only if they are no weaker than what is explicitly
written on the type occurrence.  That was a lot better than implementing
the other solutions and having to undo them later.

> Also, I proposed to add two additional checks in the BaseTypeChecker:  
> an annotated type sanity check (checking that all annotations are  
> actually valid, e.g. cannot have @Mutable String),

I agree this could go in the base checker.  For implicit annotations
(those inherited from a class declaration, as in the case of String), then
the same code mentioned above -- for determining the effective annotation
at a location -- could do this check.  Otherwise, the check can just be
that the type factory does not return two annotations that are related in
the hierarchy.  I think this can be in the base type factory.

> and method  
> invocation check (cannot call a method whose receiver type isn't a  
> subtype of the expression receiver type, cannot call an immutable  
> reference on a mutable reference).

Shouldn't this already be checked in the framework?  The framework is
supposed to already handle assignments and pseudo-assignments (examples of
pseudo-assignments are between method actuals and formals).  If not, I
presume it's a simple fix to add a receiver check to wherever the other
parameters are checked, and won't require much new code/logic.

                    -Mike