checker-framework/checker/tests/nullness/NonNullIfReturnsTest.java at 1eecfca16db3fd2126b98e7e0e9353614a1f0bfe · eisop/checker-framework · GitHub

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
153
154
155
156
157
158
159
160
161
162
// Tests @NonNullIfReturns, @NonNullIfReturnsTrue, and @NonNullIfReturnsFalse (parameter-level
// conditional postconditions) for both correct refinement and expected errors.

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.NonNullIfReturns;
import org.checkerframework.checker.nullness.qual.NonNullIfReturnsFalse;
import org.checkerframework.checker.nullness.qual.NonNullIfReturnsTrue;
import org.checkerframework.checker.nullness.qual.Nullable;

public class NonNullIfReturnsTest {

    // -----------------------------------------------------------------------
    // @NonNullIfReturns(true) / (false)
    // -----------------------------------------------------------------------

    public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
        return (str != null && !str.isEmpty());
    }

    void useHasLength(@Nullable String s) {
        if (hasLength(s)) {
            @NonNull String n = s;
            n.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull String n = s;
        }
    }

    @Override
    public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
        return this == other;
    }

    void useEquals(NonNullIfReturnsTest a, @Nullable Object b) {
        if (a.equals(b)) {
            @NonNull Object n = b;
            n.hashCode();
        }
    }

    public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
        return obj == null;
    }

    void useIsNull(@Nullable Object p) {
        if (!isNull(p)) {
            @NonNull Object n = p;
            n.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object n = p;
        }
    }

    public static boolean bothNonNull(
            @NonNullIfReturns(true) @Nullable Object a,
            @NonNullIfReturns(true) @Nullable Object b) {
        return a != null && b != null;
    }

    void useBothNonNull(@Nullable Object x, @Nullable Object y) {
        if (bothNonNull(x, y)) {
            @NonNull Object nx = x;
            @NonNull Object ny = y;
            nx.hashCode();
            ny.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object nx = x;
            // :: error: (assignment.type.incompatible)
            @NonNull Object ny = y;
        }
    }

    // Checker trusts the annotation; does not verify method body.
    public boolean alwaysTrue(@NonNullIfReturns(true) @Nullable Object obj) {
        return true;
    }

    void useAlwaysTrue(@Nullable Object p) {
        if (alwaysTrue(p)) {
            @NonNull Object n = p;
            n.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object n = p;
        }
    }

    // -----------------------------------------------------------------------
    // @NonNullIfReturnsTrue
    // -----------------------------------------------------------------------

    public static boolean hasLengthTrue(@NonNullIfReturnsTrue @Nullable String str) {
        return (str != null && !str.isEmpty());
    }

    void useHasLengthTrue(@Nullable String s) {
        if (hasLengthTrue(s)) {
            @NonNull String n = s;
            n.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull String n = s;
        }
    }

    public static boolean bothNonNullTrue(
            @NonNullIfReturnsTrue @Nullable Object a, @NonNullIfReturnsTrue @Nullable Object b) {
        return a != null && b != null;
    }

    void useBothNonNullTrue(@Nullable Object x, @Nullable Object y) {
        if (bothNonNullTrue(x, y)) {
            @NonNull Object nx = x;
            @NonNull Object ny = y;
            nx.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object nx = x;
            // :: error: (assignment.type.incompatible)
            @NonNull Object ny = y;
        }
    }

    // -----------------------------------------------------------------------
    // @NonNullIfReturnsFalse
    // -----------------------------------------------------------------------

    public static boolean isNullFalse(@NonNullIfReturnsFalse @Nullable Object obj) {
        return obj == null;
    }

    void useIsNullFalse(@Nullable Object p) {
        if (!isNullFalse(p)) {
            @NonNull Object n = p;
            n.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object n = p;
        }
    }

    public static boolean neitherNull(
            @NonNullIfReturnsFalse @Nullable Object a, @NonNullIfReturnsFalse @Nullable Object b) {
        return a == null || b == null;
    }

    void useNeitherNull(@Nullable Object x, @Nullable Object y) {
        if (!neitherNull(x, y)) {
            @NonNull Object nx = x;
            @NonNull Object ny = y;
            nx.hashCode();
        } else {
            // :: error: (assignment.type.incompatible)
            @NonNull Object nx = x;
            // :: error: (assignment.type.incompatible)
            @NonNull Object ny = y;
        }
    }
}