File: RequiresNonNullTest.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 23,104 kB
  • sloc: java: 145,916; xml: 839; sh: 518; makefile: 404; perl: 26
file content (152 lines) | stat: -rw-r--r-- 4,576 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.Pure;

class RequiresNonNullTest {

    @Nullable Object field1;
    @Nullable Object field2;

    @RequiresNonNull("field1")
    void method1() {
        field1.toString(); // OK, field1 is known to be non-null
        this.field1.toString(); // OK, field1 is known to be non-null
        // :: error: (dereference.of.nullable)
        field2.toString(); // error, might throw NullPointerException
    }

    @RequiresNonNull("field1")
    void method1also() {
        // ok, precondition satisfied by NNOE
        method1();
    }

    void method2() {
        field1 = new Object();
        method1(); // OK, satisfies method precondition
        field1 = null;
        // :: error: (contracts.precondition.not.satisfied)
        method1(); // error, does not satisfy method precondition
    }

    protected @Nullable Object field;

    @RequiresNonNull("field")
    public void requiresNonNullField() {}

    public void clientFail(RequiresNonNullTest arg1) {
        // :: error: (contracts.precondition.not.satisfied)
        arg1.requiresNonNullField();
    }

    public void clientOK(RequiresNonNullTest arg2) {
        arg2.field = new Object();
        // note that the following line works
        @NonNull Object o = arg2.field;

        arg2.requiresNonNullField(); // OK, field is known to be non-null
    }

    // TODO: forbid the field in @NNOE to be less visible than the method

    protected static @Nullable Object staticfield;

    @Pure
    @RequiresNonNull("staticfield")
    // :: warning: (purity.deterministic.void.method)
    public void reqStaticName() {
        reqStaticQualName();
    }

    @Pure
    @RequiresNonNull("RequiresNonNullTest.staticfield")
    // :: warning: (purity.deterministic.void.method)
    public void reqStaticQualName() {
        reqStaticName();
    }

    public void statClientOK(RequiresNonNullTest arg1) {
        staticfield = new Object();
        arg1.reqStaticName();

        staticfield = new Object();
        arg1.reqStaticQualName();

        RequiresNonNullTest.staticfield = new Object();
        arg1.reqStaticName();
        RequiresNonNullTest.staticfield = new Object();
        arg1.reqStaticQualName();
    }

    public void statClientFail(RequiresNonNullTest arg1) {
        // :: error: (contracts.precondition.not.satisfied)
        arg1.reqStaticName();
        // :: error: (contracts.precondition.not.satisfied)
        arg1.reqStaticQualName();
    }

    class NNOESubTest extends RequiresNonNullTest {
        public void subClientOK(NNOESubTest arg3) {
            arg3.field = new Object();
            arg3.requiresNonNullField();
        }

        public void subClientFail(NNOESubTest arg4) {
            // :: error: (contracts.precondition.not.satisfied)
            arg4.requiresNonNullField();
        }

        public void subStat(NNOESubTest arg5) {
            RequiresNonNullTest.staticfield = new Object();
            arg5.reqStaticQualName();

            staticfield = new Object();
            arg5.reqStaticQualName();

            NNOESubTest.staticfield = new Object();
            arg5.reqStaticQualName();
        }
    }

    private @Nullable Object notHidden;

    class NNOEHidingTest extends RequiresNonNullTest {

        protected @Nullable String field;

        public void hidingClient1(NNOEHidingTest arg5) {
            arg5.field = "ha!";
            /* We should be testing that the Object "field" from the superclass
             * is non-null. We currently only match on the field name and do not
             * handle hiding correctly. Instead, we output an error, if we
             * detect that hiding happened.
             * TODO: correctly resolve hidden fields.
             */
            arg5.requiresNonNullField();
        }

        public void hidingClient2(NNOEHidingTest arg6) {
            // :: error: (contracts.precondition.not.satisfied)
            arg6.requiresNonNullField();
        }

        protected @Nullable Object notHidden;

        @RequiresNonNull("notHidden")
        void notHiddenTest() {
            // the field in the superclass is private -> don't complain about hiding
        }
    }

    static @Nullable Object o = "m";

    @RequiresNonNull("o")
    void test() {
        o = null;
    }

    @RequiresNonNull("thisShouldIssue1Error")
    // Test case for Issue 1051
    // https://github.com/typetools/checker-framework/issues/1051
    // :: error: (flowexpr.parse.error)
    void testIssue1051() {}
}