[Checkers] Questions about javari checker issues
mahmood at MIT.EDU
Tue Apr 15 19:20:21 EDT 2008
I am writing this email without reviewing the code. So the names
might be off. Unfortunately, I am behind in improving the
documentation. There is some lame documentation here and there. You
might like to review GraphSubtypeRelations and TypesRelations (and see
how IGJ deals with it). Improving the documentation is my top
> 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?
I emailed you the batch earlier that deals with Javari. It dealt with
GraphSubtypeRelations. I believe that you don't need to override
anything in GraphSubtypeRelations, but you can simply specify the
relations in the regular manner.
To override the behavior of type arguments subtyping, you just need to
override compareTypeArguments in TypesRelations (check out the code in
IGJ, in IGJChecker).
> 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
> 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
> ~/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?
We have not implemented skipClasses in the framework. We should have
done it, but we didn't :(. Thanks for the reminder.
As a side note, I thought that you couldn't annotate Object.java in
source, because the compiler JVM actually needing java.lang.Object and
using a stub would break it?!
More information about the checkers