[Checkers] Questions about javari checker issues

[Telmo]

Two points:

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>, which seems a high priority bug. Implementation-wise, I 
think I should override more methods on JavariChecker to behave 
differently once the assignment check is being done on type parameters, 
instead of main types. Matt tells me that Mahmood's GraphSubtypeRelation 
proposal might change that, and/or might change the way this must be 
fixed. Should I try to fix this bug as it is now, try to change into 
GraphSubtypeRelation myself (requiring catching up on its implementation), 
or wait for Mahmood to perform the change?


B. When I run

leek:~/research/to-annotate/jolden> javac -cp ~/checkers/checkers.jar -sourcepath ~/checkers/jdk/javari/src -typeprocessor checkers.javari.JavariChecker bh/*.java

I obtain checker errors caused by incomplete jdk annotations, for example:

bh/BH.java:136: cannot invoke a Mutable method from a ReadOnly reference
       } else if (arg.equals("-s")) {
                            ^
bh/BH.java:138: incompatible types.
found   : @ReadOnly String
required: @Mutable String
           nsteps = new Integer(args[i++]).intValue();
                                    ^
bh/BH.java:142: cannot invoke a Mutable method from a ReadOnly reference
       } else if (arg.equals("-m")) {
                            ^
bh/BH.java:144: cannot invoke a Mutable method from a ReadOnly reference
       } else if (arg.equals("-p")) {
                            ^
bh/BH.java:146: cannot invoke a Mutable method from a ReadOnly reference
       } else if (arg.equals("-h")) {
                            ^

among other errors I need to fix (such as allowing annotations on static 
method receivers for javari, that will then apply only to static local 
fields, since the other fields cannot be referred to according to regular 
java syntax, and possibly manual annotation errors).

~/checkers/jdk/javari/src/java/lang/Object.java, however, is properly 
annotated. Unfortunately, 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?

-Telmo