[Checkers] Questions about javari checker issues

[Michael Ernst]

Telmo-

> A. Mahmood pointed to me that as of the last release, the Javari checker 
> doesn't emit errors for an assignment of a type A<@Mutable B> into a type 
> A<@ReadOnly B>,

Mahmood, thanks for noting this.

Telmo, if the current framework is inadequately documented, then it may
make sense to wait, since the documentation is supposed to be high on
Mahmood's priority list.  If Mahmood is still in the process of improving
the framework to make this easy for you to do, that would be another
argument for delaying.

> I obtain checker errors caused by incomplete jdk annotations, for example:
> ...
> the annotations on String.java are not as 
> complete as they should be (for instance, equals doesn't have a @ReadOnly 
> receiver annotation). The checker doesn't complain about it since the jdk 
> is not being type-checked, but the bh test of jolden doesn't pass. What 
> should be done about this?

If notice a problem with some annotation on a library class, you should
improve all the annotations on that class.  In this case, if String.equals
has a problem, you should go through all of String and make sure that the
annotations are correct.  (And this is something that Matt and Mahmood must
do as well.)  Ideally, you would make the fixes package by package rather
than class by class.

This will take time, but it is absolutely critical for usability.  Such
problems will annoy users just as much as a bug in your checker.  And, you
can diagnose and fix library problems more easily than other users can.

Mahmood said:
> When I was annotating the JDK, I found it very helpful to type check  
> the jdk stubs with the checker.  It informed of many missing  
> annotations (because of the override relationship check).

This is a good idea, too.

                    -Mike