Message improvement request: contracts.conditional.postcondition contract is unclear

[vlsi]

Error message:

Sample code (see https://github.com/apache/calcite/blob/103430bcc76ed1a7cbab6861ecdd39814cf4ef83/core/src/main/java/org/apache/calcite/util/ImmutableIntList.java#L115-L121 ):

  @Override public boolean equals(@Nullable Object obj) {
    return this == obj
        || obj instanceof ImmutableIntList
        ? Arrays.equals(ints, ((ImmutableIntList) obj).ints)
        : obj instanceof List
            && obj.equals(this);
  }

Error message:

ImmutableIntList.java:120: error: [contracts.conditional.postcondition.not.satis
fied] the conditional postcondition about 'EnsuresNonNullIf' at this return statement is not satisfied
    return this == obj
    ^

Unfortunately, it is hard to tell what went wrong.
What if checker-framework printed the contract in question, so users could figure out what went wrong.

PS. I think the error is false-positive

[mernst]

I agree that error message is quite confusing and should be improved. Thank you for reporting it.

#3621 will change the message to:

ImmutableIntList.java:120: error: [contracts.conditional.postcondition.not.satisfied] conditional postcondition is not satisfied when equals returns true.
      return this == obj
      ^
  found   : obj is @Nullable
  required: obj is @NonNull

Let me know whether that is clear enough, or if you have suggestions for further improving it.

[mernst]

By the way, your implementation of equals looks like it calls Arrays.equals even if this == obj is true. (That yields correct results, but is unnecessarily inefficient.) The precedence rules of Java are confusing, but I think you could change the code to

  @Override
  public boolean equals(@Nullable Object obj) {
    return this == obj
        || (obj instanceof ImmutableIntList
            ? Arrays.equals(ints, ((ImmutableIntList) obj).ints)
            : obj instanceof List && obj.equals(this));
  }

or

  @Override
  public boolean equals(@Nullable Object obj) {
    if (this == obj) {
      return true;
    }
    return obj instanceof ImmutableIntList
        ? Arrays.equals(ints, ((ImmutableIntList) obj).ints)
        : obj instanceof List
            && obj.equals(this);
  }

[mernst]

I have opened a new issue, #3622, to track the fact that the warning is a false positive.

[vlsi]

Oh, you are right this can be improved. I was focused more on annotating nullness, and I did not want to break code by accident :)

ImmutableIntList.java:120: error: [contracts.conditional.postcondition.not.satisfied] conditional postcondition is not satisfied when equals returns true.
      return this == obj
      ^
  found   : obj is @Nullable
  required: obj is @NonNull

Wow! It would be much better.