[Checkers] Suggestions for NonNull checker warning messages

[Michael Ernst]

Matt-

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?  In that case, I think
it would be much clearer to simply so state:  say that there might be a
null pointer exception.  A better message is:

  Receiver may be null

or

  Reciever debug may be null

or

  Receiver may be null:  debug

or

  Possibly-null receiver debug


2. Another puzzling case is warnings like these:

./daikon/inv/unary/sequence/NoDuplicates.java:116: incompatible types.
found   : @Nullable String
required: @NonNull String
      + form[3];
      ^
./daikon/inv/unary/sequence/NoDuplicates.java:120: incompatible types.
found   : @Nullable String
required: @NonNull String
    return "daikon.Quant.noDups(" + var().name_using(format) + ")";
                                                             ^
./daikon/inv/unary/sequence/EltwiseFloatGreaterThan.java:103: incompatible types.
found   : @Nullable String
required: @NonNull String
    /*@NonNull*/ String result = quant.getQuantifierExp() + "(" + quant.getMembershipRestriction(0) + " /\\ " + quant.getMembershipRestriction(1);
                                                                                                              ^

You can see the code being checked in the second and third cases.
(But, I haven't been successful in creating a small test case for the test
suite.)
The code being checked in the first is this:

  /*@NonNull*/ public String format_simplify() /*@Raw*/  {
    /*@NonNull*/ String[] form = VarInfo.simplify_quantify (QuantFlags.distinct(), var(),
                                               var());
    return form[0] + "(NEQ " + form[1] + " " + form[2] + ")"
      + form[3];
  }

I don't think the problem is with String concatenation -- the checker
passes this method:

  public @NonNull String stringConcatenation(boolean b) {
    if (b)
      return "foo" + null;
    else
      return null + "foo";
  }

so I am not sure how to interpret the checker warning.

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)) {
               ^

Rather than saying "cannot dereference", I think it's better to state the
possible consequence.  How about something like
  Dereference of possibly-null reference vis[0]
  Possible null pointer exception when dereferencing possibly-null reference vis[0]
  Possibly null pointer exception when dereferencing vis[0]

One thing I really like about this error message, though is that it
explicitly states the name of the reference, "vis[0]".  That is very
helpful, so please retain it, and consider including it in other messages.

                     Thanks,

                    -Mike