PolyNull Object as receiver error

[Ao-senXiong]

In this code snippet, the expected error is dereferenc of possibly-null reference nbl. However, a method invocation invalid error is also raised.

import org.checkerframework.checker.nullness.qual.PolyNull;

class Demo {
    void foo(@PolyNull Object nbl) {
        if (nbl == null) {
            nbl.toString();
        }
    }
}

Error message is listing for reference:

Demo.java:6: error: [dereference.of.nullable] dereference of possibly-null reference nbl
            nbl.toString();
            ^
Demo.java:6: error: [method.invocation.invalid] call to toString() not allowed on the given receiver.
            nbl.toString();
                        ^
  found   : @FBCBottom @PolyNull Object
  required: @Initialized @NonNull Object

Another code snippet with @Nullable annotation is

import org.checkerframework.checker.nullness.qual.Nullable;

class Demo {
    void foo(@Nullable Object nbl) {
        if (nbl == null) {
            nbl.toString();
        }
    }
}

And the corresponding error message are listing below

Demo.java:6: error: [dereference.of.nullable] dereference of possibly-null reference nbl
            nbl.toString();
            ^
1 error

[wmdietl]

This came up here: #525 (comment) . Try to keep references between different issues and PRs, to make the history easier to follow.

It's noteworthy here that a different error is issued for @Nullable instead of @PolyNull in this test case.

[Ao-senXiong]

This came up here: #525 (comment) . Try to keep references between different issues and PRs, to make the history easier to follow.

It's noteworthy here that a different error is issued for @Nullable instead of @PolyNull in this test case.

Thanks, already added.

[Ao-senXiong]

For a simpler case without dataflow refinement, I think we are still expecting to dereference possible-null reference errors because of soundness.

import org.checkerframework.checker.nullness.qual.PolyNull;

class Demo {
    void foo(@PolyNull Object nbl) {
            nbl.toString();
    }
}

[wmdietl]

Yes, directly dereferencing a PolyNull reference should give you an error, like for a Nullable reference.