| import org.checkerframework.checker.nullness.qual.Nullable; |
| |
| class Upper { |
| @Nullable String fs = "NonNull init"; |
| final @Nullable String ffs = "NonNull init"; |
| |
| void access() { |
| // Error, because non-final field type is not refined |
| // :: error: (dereference.of.nullable) |
| fs.hashCode(); |
| // Final field in the same class is refined |
| ffs.hashCode(); |
| } |
| } |
| |
| public class FinalFields { |
| public void foo(Upper u) { |
| // Error, because final field in different class is not refined |
| // :: error: (dereference.of.nullable) |
| u.fs.hashCode(); |
| } |
| |
| public void bar(Lower l) { |
| // Error, because final field in different class is not refined |
| // :: error: (dereference.of.nullable) |
| l.fs.hashCode(); |
| } |
| |
| public void local() { |
| @Nullable String ls = "Locals"; |
| // Local variable is refined |
| ls.hashCode(); |
| } |
| } |
| |
| class Lower { |
| @Nullable String fs = "NonNull init, too"; |
| final @Nullable String ffs = "NonNull init, too"; |
| |
| void access() { |
| // Error, because non-final field type is not refined |
| // :: error: (dereference.of.nullable) |
| fs.hashCode(); |
| // Final field in the same class is refined |
| ffs.hashCode(); |
| } |
| } |