[Checkers] Suggestions for NonNull checker warning messages

[Matt Papi]

Mike,

>  1. I'm having trouble interpreting this error message.
>
>  ./daikon/inv/unary/sequence/NoDuplicates.java:71: call to isLoggable(java.util.logging.Level) not allowed on the given receiver.
>  found   : @Nullable Logger
>  required: @NonNull Logger
>     if (debug.isLoggable(Level.FINE)) {
>                         ^
>
>  Does it just mean that the receiver might be null?

Yes, but this comes from functionality inherited from the framework
that (in this case) is difficult to override. There's a single message
key that is used when a method is not invokable on its receiver, and
the NonNull checker should really use a different message depending on
whether the receiver is @Raw or @NonNull (calling a non- at Raw method
from a constructor is not an illegal dereference -- it's an invalid
invocation in the same way as calling a method with a @Mutable
receiver on a @ReadOnly reference).

Since the framework, not the checker, is emitting the message, we'd
have to either carefully alter the framework or add a whole lot of
boilerplate to NonNullChecker (which currently has no methods).
Mahmood, do you have any thoughts on this?


>  2. Another puzzling case is warnings like these:
>  [snip]

All of those warnings are coming from the framework (which is also
responsible for the placement of the "^"). The reason is not
immediately obvious to me, but I'll take a look.


>  3. This error message is not very helpful, either.
>
>  ./daikon/inv/unary/sequence/NoDuplicates.java:152: cannot dereference the possibly-null reference vis[0]
>     if (!vis[0].aux.getFlag(VarInfoAux.HAS_DUPLICATES)) {
>                ^

Sure, that one is trivial to fix. I like "dereference of possibly-null
reference vis[0]", so I'll probably change to that one.


- Matt