@RequiresNonNull and field visibilty

[GoogleCodeExporter]

Hi,

from what I gather @RequiresNonNull should be enforced by the nullness checker 
but I can't get it to work.

I have this (condensed) test case that produces no errors for these classes, 
only warnings about missing documentation:

class ClassA {
    @Nullable private String value = null;

    @RequiresNonNull("value") public String getValue() {
        return value;
    }
}

public class Tester {
    public static void main(String[] args) {
        ClassA a = new ClassA();
        a.getValue();
    }
}

No error is reported even with
@MonotonicNonNull private String value;
which is what I had in the beginning, but then I tried and noticed that it 
doesn't work even with the code above that explicitly sets the field to null.

I'm using version 1.8.9 with NetBeans 8.0.2 x64, Ant 1.9.4 and the javac 
included in JDK 1.8.0_u25 x64 on Windows 8.
I pass these options to the compiler:
-version -Xlint:all -Xdoclint:all

My ant target is attached.

The nullness checker seems to work fine otherwise, I can see various errors for 
other classes that seem sensible and I already have added some annotations to 
eliminate errors.
So I think that the issue, if there's any, is related to the particular 
annotations used in the sample above.

Original issue reported on code.google.com by karlsand...@gmail.com on 11 Jan 2015 at 9:22

Attachments:

• [Ant Task.xml](https://storage.googleapis.com/google-code-attachments/checker-framework/issue-391/comment-0/Ant Task.xml)

[GoogleCodeExporter]

Thanks for the bug report!
The issue is that field "value" is private. When you make the field 
default/public, you get the expected error message:

Issue391.java:14: error: [contracts.precondition.not.satisfied] the called 
method 'a.getValue()' has a precondition 'a.value' that is not satisfied
        a.getValue();

The problem is that when the field is private, the caller doesn't know about 
the field and has no way of setting it. So at the moment we don't issue errors 
for such fields.
We should discuss the interaction between visibility and pre/post-conditions, 
which has been on our list.

Original comment by wdi...@gmail.com on 11 Jan 2015 at 3:20

• Changed title: @RequiresNonNull and field visibilty
• Changed state: Accepted

[GoogleCodeExporter]

A simple approach is to treat that all private fields and methods as 
spec-public.
(I thought this was already how the Checker Framework behaved.)  I think this 
is a reasonable tradeoff between complexity and expressiveness.

I do think it's important that a checker should issue a warning even when the 
field is private.

Original comment by michael.ernst@gmail.com on 12 Jan 2015 at 11:31

[GoogleCodeExporter]

Thank you very much for your replies.

Since I would love to have @RequiresNonNull and @EnsuresNonNull* working with 
private fields I had a look at the classes in package 
org.checkerframework.checker.nullness for a place where I could modify the code 
to obtain the desired effect but I couldn't find anything.

So, provided it's a small change, I'd like to have a hint on where to look.
This way if you decide that it's not appropriate to change the framework I can 
still use a patched version.

Original comment by karlsand...@gmail.com on 12 Jan 2015 at 12:03

[GoogleCodeExporter]

Original comment by mcart...@cs.washington.edu on 15 Jan 2015 at 4:25

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 8 Apr 2015 at 9:10